Theorem wemaplem2 8452

Description: Lemma for wemapso 8456. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.)

Hypotheses

Ref	Expression
wemapso.t	|- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
wemaplem2.a	|- ( ph -> A e. _V )
wemaplem2.p	|- ( ph -> P e. ( B ^m A ) )
wemaplem2.x	|- ( ph -> X e. ( B ^m A ) )
wemaplem2.q	|- ( ph -> Q e. ( B ^m A ) )
wemaplem2.r	|- ( ph -> R Or A )
wemaplem2.s	|- ( ph -> S Po B )
wemaplem2.px1	|- ( ph -> a e. A )
wemaplem2.px2	|- ( ph -> ( P ` a ) S ( X ` a ) )
wemaplem2.px3	|- ( ph -> A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) )
wemaplem2.xq1	|- ( ph -> b e. A )
wemaplem2.xq2	|- ( ph -> ( X ` b ) S ( Q ` b ) )
wemaplem2.xq3	|- ( ph -> A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) )

Assertion

Ref	Expression
wemaplem2	|- ( ph -> P T Q )

Distinct variable groups:   a, b, c, x, B   T, a, b, c   w, a, y, z, X, b, c, x   A, a, b, c, w, x, y, z   P, a, b, c, w, x, y, z   Q, a, b, c, w, x, y, z   R, a, b, c, w, x, y, z   S, a, b, c, w, x, y, z

Allowed substitution hints:   ph( x, y, z, w, a, b, c)   B( y, z, w)   T( x, y, z, w)

Proof of Theorem wemaplem2

Dummy variable d is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wemaplem2.px1	. . . 4 |- ( ph -> a e. A )
2		wemaplem2.xq1	. . . 4 |- ( ph -> b e. A )
3	1, 2	ifcld 4131	. . 3 |- ( ph -> if ( a R b , a , b ) e. A )
4		wemaplem2.px2	. . . . . . 7 |- ( ph -> ( P ` a ) S ( X ` a ) )
5	4	adantr 481	. . . . . 6 |- ( ( ph /\ a R b ) -> ( P ` a ) S ( X ` a ) )
6		wemaplem2.xq3	. . . . . . . 8 |- ( ph -> A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) )
7		breq1 4656	. . . . . . . . . 10 |- ( c = a -> ( c R b <-> a R b ) )
8		fveq2 6191	. . . . . . . . . . 11 |- ( c = a -> ( X ` c ) = ( X ` a ) )
9		fveq2 6191	. . . . . . . . . . 11 |- ( c = a -> ( Q ` c ) = ( Q ` a ) )
10	8, 9	eqeq12d 2637	. . . . . . . . . 10 |- ( c = a -> ( ( X ` c ) = ( Q ` c ) <-> ( X ` a ) = ( Q ` a ) ) )
11	7, 10	imbi12d 334	. . . . . . . . 9 |- ( c = a -> ( ( c R b -> ( X ` c ) = ( Q ` c ) ) <-> ( a R b -> ( X ` a ) = ( Q ` a ) ) ) )
12	11	rspcva 3307	. . . . . . . 8 |- ( ( a e. A /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> ( a R b -> ( X ` a ) = ( Q ` a ) ) )
13	1, 6, 12	syl2anc 693	. . . . . . 7 |- ( ph -> ( a R b -> ( X ` a ) = ( Q ` a ) ) )
14	13	imp 445	. . . . . 6 |- ( ( ph /\ a R b ) -> ( X ` a ) = ( Q ` a ) )
15	5, 14	breqtrd 4679	. . . . 5 |- ( ( ph /\ a R b ) -> ( P ` a ) S ( Q ` a ) )
16		iftrue 4092	. . . . . . . 8 |- ( a R b -> if ( a R b , a , b ) = a )
17	16	fveq2d 6195	. . . . . . 7 |- ( a R b -> ( P ` if ( a R b , a , b ) ) = ( P ` a ) )
18	16	fveq2d 6195	. . . . . . 7 |- ( a R b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` a ) )
19	17, 18	breq12d 4666	. . . . . 6 |- ( a R b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` a ) S ( Q ` a ) ) )
20	19	adantl 482	. . . . 5 |- ( ( ph /\ a R b ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` a ) S ( Q ` a ) ) )
21	15, 20	mpbird 247	. . . 4 |- ( ( ph /\ a R b ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
22		wemaplem2.s	. . . . . . 7 |- ( ph -> S Po B )
23	22	adantr 481	. . . . . 6 |- ( ( ph /\ a = b ) -> S Po B )
24		wemaplem2.p	. . . . . . . . . 10 |- ( ph -> P e. ( B ^m A ) )
25		elmapi 7879	. . . . . . . . . 10 |- ( P e. ( B ^m A ) -> P : A --> B )
26	24, 25	syl 17	. . . . . . . . 9 |- ( ph -> P : A --> B )
27	26, 2	ffvelrnd 6360	. . . . . . . 8 |- ( ph -> ( P ` b ) e. B )
28		wemaplem2.x	. . . . . . . . . 10 |- ( ph -> X e. ( B ^m A ) )
29		elmapi 7879	. . . . . . . . . 10 |- ( X e. ( B ^m A ) -> X : A --> B )
30	28, 29	syl 17	. . . . . . . . 9 |- ( ph -> X : A --> B )
31	30, 2	ffvelrnd 6360	. . . . . . . 8 |- ( ph -> ( X ` b ) e. B )
32		wemaplem2.q	. . . . . . . . . 10 |- ( ph -> Q e. ( B ^m A ) )
33		elmapi 7879	. . . . . . . . . 10 |- ( Q e. ( B ^m A ) -> Q : A --> B )
34	32, 33	syl 17	. . . . . . . . 9 |- ( ph -> Q : A --> B )
35	34, 2	ffvelrnd 6360	. . . . . . . 8 |- ( ph -> ( Q ` b ) e. B )
36	27, 31, 35	3jca 1242	. . . . . . 7 |- ( ph -> ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) )
37	36	adantr 481	. . . . . 6 |- ( ( ph /\ a = b ) -> ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) )
38		fveq2 6191	. . . . . . . . 9 |- ( a = b -> ( P ` a ) = ( P ` b ) )
39		fveq2 6191	. . . . . . . . 9 |- ( a = b -> ( X ` a ) = ( X ` b ) )
40	38, 39	breq12d 4666	. . . . . . . 8 |- ( a = b -> ( ( P ` a ) S ( X ` a ) <-> ( P ` b ) S ( X ` b ) ) )
41	4, 40	syl5ibcom 235	. . . . . . 7 |- ( ph -> ( a = b -> ( P ` b ) S ( X ` b ) ) )
42	41	imp 445	. . . . . 6 |- ( ( ph /\ a = b ) -> ( P ` b ) S ( X ` b ) )
43		wemaplem2.xq2	. . . . . . 7 |- ( ph -> ( X ` b ) S ( Q ` b ) )
44	43	adantr 481	. . . . . 6 |- ( ( ph /\ a = b ) -> ( X ` b ) S ( Q ` b ) )
45		potr 5047	. . . . . . 7 |- ( ( S Po B /\ ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) ) -> ( ( ( P ` b ) S ( X ` b ) /\ ( X ` b ) S ( Q ` b ) ) -> ( P ` b ) S ( Q ` b ) ) )
46	45	imp 445	. . . . . 6 |- ( ( ( S Po B /\ ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) ) /\ ( ( P ` b ) S ( X ` b ) /\ ( X ` b ) S ( Q ` b ) ) ) -> ( P ` b ) S ( Q ` b ) )
47	23, 37, 42, 44, 46	syl22anc 1327	. . . . 5 |- ( ( ph /\ a = b ) -> ( P ` b ) S ( Q ` b ) )
48		ifeq1 4090	. . . . . . . . 9 |- ( a = b -> if ( a R b , a , b ) = if ( a R b , b , b ) )
49		ifid 4125	. . . . . . . . 9 |- if ( a R b , b , b ) = b
50	48, 49	syl6eq 2672	. . . . . . . 8 |- ( a = b -> if ( a R b , a , b ) = b )
51	50	fveq2d 6195	. . . . . . 7 |- ( a = b -> ( P ` if ( a R b , a , b ) ) = ( P ` b ) )
52	50	fveq2d 6195	. . . . . . 7 |- ( a = b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` b ) )
53	51, 52	breq12d 4666	. . . . . 6 |- ( a = b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
54	53	adantl 482	. . . . 5 |- ( ( ph /\ a = b ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
55	47, 54	mpbird 247	. . . 4 |- ( ( ph /\ a = b ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
56		wemaplem2.px3	. . . . . . . 8 |- ( ph -> A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) )
57		breq1 4656	. . . . . . . . . 10 |- ( c = b -> ( c R a <-> b R a ) )
58		fveq2 6191	. . . . . . . . . . 11 |- ( c = b -> ( P ` c ) = ( P ` b ) )
59		fveq2 6191	. . . . . . . . . . 11 |- ( c = b -> ( X ` c ) = ( X ` b ) )
60	58, 59	eqeq12d 2637	. . . . . . . . . 10 |- ( c = b -> ( ( P ` c ) = ( X ` c ) <-> ( P ` b ) = ( X ` b ) ) )
61	57, 60	imbi12d 334	. . . . . . . . 9 |- ( c = b -> ( ( c R a -> ( P ` c ) = ( X ` c ) ) <-> ( b R a -> ( P ` b ) = ( X ` b ) ) ) )
62	61	rspcva 3307	. . . . . . . 8 |- ( ( b e. A /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) -> ( b R a -> ( P ` b ) = ( X ` b ) ) )
63	2, 56, 62	syl2anc 693	. . . . . . 7 |- ( ph -> ( b R a -> ( P ` b ) = ( X ` b ) ) )
64	63	imp 445	. . . . . 6 |- ( ( ph /\ b R a ) -> ( P ` b ) = ( X ` b ) )
65	43	adantr 481	. . . . . 6 |- ( ( ph /\ b R a ) -> ( X ` b ) S ( Q ` b ) )
66	64, 65	eqbrtrd 4675	. . . . 5 |- ( ( ph /\ b R a ) -> ( P ` b ) S ( Q ` b ) )
67		wemaplem2.r	. . . . . . . . 9 |- ( ph -> R Or A )
68		sopo 5052	. . . . . . . . 9 |- ( R Or A -> R Po A )
69	67, 68	syl 17	. . . . . . . 8 |- ( ph -> R Po A )
70		po2nr 5048	. . . . . . . 8 |- ( ( R Po A /\ ( b e. A /\ a e. A ) ) -> -. ( b R a /\ a R b ) )
71	69, 2, 1, 70	syl12anc 1324	. . . . . . 7 |- ( ph -> -. ( b R a /\ a R b ) )
72		nan 604	. . . . . . 7 |- ( ( ph -> -. ( b R a /\ a R b ) ) <-> ( ( ph /\ b R a ) -> -. a R b ) )
73	71, 72	mpbi 220	. . . . . 6 |- ( ( ph /\ b R a ) -> -. a R b )
74		iffalse 4095	. . . . . . . 8 |- ( -. a R b -> if ( a R b , a , b ) = b )
75	74	fveq2d 6195	. . . . . . 7 |- ( -. a R b -> ( P ` if ( a R b , a , b ) ) = ( P ` b ) )
76	74	fveq2d 6195	. . . . . . 7 |- ( -. a R b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` b ) )
77	75, 76	breq12d 4666	. . . . . 6 |- ( -. a R b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
78	73, 77	syl 17	. . . . 5 |- ( ( ph /\ b R a ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
79	66, 78	mpbird 247	. . . 4 |- ( ( ph /\ b R a ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
80		solin 5058	. . . . 5 |- ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( a R b \/ a = b \/ b R a ) )
81	67, 1, 2, 80	syl12anc 1324	. . . 4 |- ( ph -> ( a R b \/ a = b \/ b R a ) )
82	21, 55, 79, 81	mpjao3dan 1395	. . 3 |- ( ph -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
83		r19.26 3064	. . . . 5 |- ( A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) <-> ( A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) )
84	56, 6, 83	sylanbrc 698	. . . 4 |- ( ph -> A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) )
85	67, 1, 2	3jca 1242	. . . . 5 |- ( ph -> ( R Or A /\ a e. A /\ b e. A ) )
86		prth 595	. . . . . . 7 |- ( ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> ( ( c R a /\ c R b ) -> ( ( P ` c ) = ( X ` c ) /\ ( X ` c ) = ( Q ` c ) ) ) )
87		eqtr 2641	. . . . . . 7 |- ( ( ( P ` c ) = ( X ` c ) /\ ( X ` c ) = ( Q ` c ) ) -> ( P ` c ) = ( Q ` c ) )
88	86, 87	syl6 35	. . . . . 6 |- ( ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) )
89	88	ralimi 2952	. . . . 5 |- ( A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> A. c e. A ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) )
90		simpl1 1064	. . . . . . . . 9 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> R Or A )
91		simpr 477	. . . . . . . . 9 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> c e. A )
92		simpl2 1065	. . . . . . . . 9 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> a e. A )
93		simpl3 1066	. . . . . . . . 9 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> b e. A )
94		soltmin 5532	. . . . . . . . 9 |- ( ( R Or A /\ ( c e. A /\ a e. A /\ b e. A ) ) -> ( c R if ( a R b , a , b ) <-> ( c R a /\ c R b ) ) )
95	90, 91, 92, 93, 94	syl13anc 1328	. . . . . . . 8 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> ( c R if ( a R b , a , b ) <-> ( c R a /\ c R b ) ) )
96	95	biimpd 219	. . . . . . 7 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> ( c R if ( a R b , a , b ) -> ( c R a /\ c R b ) ) )
97	96	imim1d 82	. . . . . 6 |- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> ( ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) -> ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) )
98	97	ralimdva 2962	. . . . 5 |- ( ( R Or A /\ a e. A /\ b e. A ) -> ( A. c e. A ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) )
99	85, 89, 98	syl2im 40	. . . 4 |- ( ph -> ( A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) )
100	84, 99	mpd 15	. . 3 |- ( ph -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) )
101		fveq2 6191	. . . . . 6 |- ( d = if ( a R b , a , b ) -> ( P ` d ) = ( P ` if ( a R b , a , b ) ) )
102		fveq2 6191	. . . . . 6 |- ( d = if ( a R b , a , b ) -> ( Q ` d ) = ( Q ` if ( a R b , a , b ) ) )
103	101, 102	breq12d 4666	. . . . 5 |- ( d = if ( a R b , a , b ) -> ( ( P ` d ) S ( Q ` d ) <-> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) ) )
104		breq2 4657	. . . . . . 7 |- ( d = if ( a R b , a , b ) -> ( c R d <-> c R if ( a R b , a , b ) ) )
105	104	imbi1d 331	. . . . . 6 |- ( d = if ( a R b , a , b ) -> ( ( c R d -> ( P ` c ) = ( Q ` c ) ) <-> ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) )
106	105	ralbidv 2986	. . . . 5 |- ( d = if ( a R b , a , b ) -> ( A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) <-> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) )
107	103, 106	anbi12d 747	. . . 4 |- ( d = if ( a R b , a , b ) -> ( ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) <-> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) /\ A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) )
108	107	rspcev 3309	. . 3 |- ( ( if ( a R b , a , b ) e. A /\ ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) /\ A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) -> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) )
109	3, 82, 100, 108	syl12anc 1324	. 2 |- ( ph -> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) )
110		wemapso.t	. . . 4 |- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
111	110	wemaplem1 8451	. . 3 |- ( ( P e. ( B ^m A ) /\ Q e. ( B ^m A ) ) -> ( P T Q <-> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) )
112	24, 32, 111	syl2anc 693	. 2 |- ( ph -> ( P T Q <-> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) )
113	109, 112	mpbird 247	1 |- ( ph -> P T Q )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   ifcif 4086   class class class wbr 4653   {copab 4712   Po wpo 5033   Or wor 5034   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859

This theorem is referenced by:  wemaplem3  8453