Metamath Proof Explorer

Theorem wemaplem2

Description: Lemma for wemapso . Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypotheses 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.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 wemaplem2 
|- ( ph -> P T Q )

Proof

Step Hyp Ref Expression
1 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 ) ) ) }
2 wemaplem2.p 
 |-  ( ph -> P e. ( B ^m A ) )
3 wemaplem2.x 
 |-  ( ph -> X e. ( B ^m A ) )
4 wemaplem2.q 
 |-  ( ph -> Q e. ( B ^m A ) )
5 wemaplem2.r 
 |-  ( ph -> R Or A )
6 wemaplem2.s 
 |-  ( ph -> S Po B )
7 wemaplem2.px1 
 |-  ( ph -> a e. A )
8 wemaplem2.px2 
 |-  ( ph -> ( P ` a ) S ( X ` a ) )
9 wemaplem2.px3 
 |-  ( ph -> A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) )
10 wemaplem2.xq1 
 |-  ( ph -> b e. A )
11 wemaplem2.xq2 
 |-  ( ph -> ( X ` b ) S ( Q ` b ) )
12 wemaplem2.xq3 
 |-  ( ph -> A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) )
13 7 10 ifcld 
 |-  ( ph -> if ( a R b , a , b ) e. A )
14 8 adantr 
 |-  ( ( ph /\ a R b ) -> ( P ` a ) S ( X ` a ) )
15 breq1 
 |-  ( c = a -> ( c R b <-> a R b ) )
16 fveq2 
 |-  ( c = a -> ( X ` c ) = ( X ` a ) )
17 fveq2 
 |-  ( c = a -> ( Q ` c ) = ( Q ` a ) )
18 16 17 eqeq12d 
 |-  ( c = a -> ( ( X ` c ) = ( Q ` c ) <-> ( X ` a ) = ( Q ` a ) ) )
19 15 18 imbi12d 
 |-  ( c = a -> ( ( c R b -> ( X ` c ) = ( Q ` c ) ) <-> ( a R b -> ( X ` a ) = ( Q ` a ) ) ) )
20 19 12 7 rspcdva 
 |-  ( ph -> ( a R b -> ( X ` a ) = ( Q ` a ) ) )
21 20 imp 
 |-  ( ( ph /\ a R b ) -> ( X ` a ) = ( Q ` a ) )
22 14 21 breqtrd 
 |-  ( ( ph /\ a R b ) -> ( P ` a ) S ( Q ` a ) )
23 iftrue 
 |-  ( a R b -> if ( a R b , a , b ) = a )
24 23 fveq2d 
 |-  ( a R b -> ( P ` if ( a R b , a , b ) ) = ( P ` a ) )
25 23 fveq2d 
 |-  ( a R b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` a ) )
26 24 25 breq12d 
 |-  ( a R b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` a ) S ( Q ` a ) ) )
27 26 adantl 
 |-  ( ( ph /\ a R b ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` a ) S ( Q ` a ) ) )
28 22 27 mpbird 
 |-  ( ( ph /\ a R b ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
29 6 adantr 
 |-  ( ( ph /\ a = b ) -> S Po B )
30 elmapi 
 |-  ( P e. ( B ^m A ) -> P : A --> B )
31 2 30 syl 
 |-  ( ph -> P : A --> B )
32 31 10 ffvelrnd 
 |-  ( ph -> ( P ` b ) e. B )
33 elmapi 
 |-  ( X e. ( B ^m A ) -> X : A --> B )
34 3 33 syl 
 |-  ( ph -> X : A --> B )
35 34 10 ffvelrnd 
 |-  ( ph -> ( X ` b ) e. B )
36 elmapi 
 |-  ( Q e. ( B ^m A ) -> Q : A --> B )
37 4 36 syl 
 |-  ( ph -> Q : A --> B )
38 37 10 ffvelrnd 
 |-  ( ph -> ( Q ` b ) e. B )
39 32 35 38 3jca 
 |-  ( ph -> ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) )
40 39 adantr 
 |-  ( ( ph /\ a = b ) -> ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) )
41 fveq2 
 |-  ( a = b -> ( P ` a ) = ( P ` b ) )
42 fveq2 
 |-  ( a = b -> ( X ` a ) = ( X ` b ) )
43 41 42 breq12d 
 |-  ( a = b -> ( ( P ` a ) S ( X ` a ) <-> ( P ` b ) S ( X ` b ) ) )
44 8 43 syl5ibcom 
 |-  ( ph -> ( a = b -> ( P ` b ) S ( X ` b ) ) )
45 44 imp 
 |-  ( ( ph /\ a = b ) -> ( P ` b ) S ( X ` b ) )
46 11 adantr 
 |-  ( ( ph /\ a = b ) -> ( X ` b ) S ( Q ` b ) )
47 potr 
 |-  ( ( 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 ) ) )
48 47 imp 
 |-  ( ( ( 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 ) )
49 29 40 45 46 48 syl22anc 
 |-  ( ( ph /\ a = b ) -> ( P ` b ) S ( Q ` b ) )
50 ifeq1 
 |-  ( a = b -> if ( a R b , a , b ) = if ( a R b , b , b ) )
51 ifid 
 |-  if ( a R b , b , b ) = b
52 50 51 eqtrdi 
 |-  ( a = b -> if ( a R b , a , b ) = b )
53 52 fveq2d 
 |-  ( a = b -> ( P ` if ( a R b , a , b ) ) = ( P ` b ) )
54 52 fveq2d 
 |-  ( a = b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` b ) )
55 53 54 breq12d 
 |-  ( a = b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
56 55 adantl 
 |-  ( ( ph /\ a = b ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
57 49 56 mpbird 
 |-  ( ( ph /\ a = b ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
58 breq1 
 |-  ( c = b -> ( c R a <-> b R a ) )
59 fveq2 
 |-  ( c = b -> ( P ` c ) = ( P ` b ) )
60 fveq2 
 |-  ( c = b -> ( X ` c ) = ( X ` b ) )
61 59 60 eqeq12d 
 |-  ( c = b -> ( ( P ` c ) = ( X ` c ) <-> ( P ` b ) = ( X ` b ) ) )
62 58 61 imbi12d 
 |-  ( c = b -> ( ( c R a -> ( P ` c ) = ( X ` c ) ) <-> ( b R a -> ( P ` b ) = ( X ` b ) ) ) )
63 62 9 10 rspcdva 
 |-  ( ph -> ( b R a -> ( P ` b ) = ( X ` b ) ) )
64 63 imp 
 |-  ( ( ph /\ b R a ) -> ( P ` b ) = ( X ` b ) )
65 11 adantr 
 |-  ( ( ph /\ b R a ) -> ( X ` b ) S ( Q ` b ) )
66 64 65 eqbrtrd 
 |-  ( ( ph /\ b R a ) -> ( P ` b ) S ( Q ` b ) )
67 sopo 
 |-  ( R Or A -> R Po A )
68 5 67 syl 
 |-  ( ph -> R Po A )
69 po2nr 
 |-  ( ( R Po A /\ ( b e. A /\ a e. A ) ) -> -. ( b R a /\ a R b ) )
70 68 10 7 69 syl12anc 
 |-  ( ph -> -. ( b R a /\ a R b ) )
71 nan 
 |-  ( ( ph -> -. ( b R a /\ a R b ) ) <-> ( ( ph /\ b R a ) -> -. a R b ) )
72 70 71 mpbi 
 |-  ( ( ph /\ b R a ) -> -. a R b )
73 iffalse 
 |-  ( -. a R b -> if ( a R b , a , b ) = b )
74 73 fveq2d 
 |-  ( -. a R b -> ( P ` if ( a R b , a , b ) ) = ( P ` b ) )
75 73 fveq2d 
 |-  ( -. a R b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` b ) )
76 74 75 breq12d 
 |-  ( -. a R b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
77 72 76 syl 
 |-  ( ( ph /\ b R a ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) )
78 66 77 mpbird 
 |-  ( ( ph /\ b R a ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
79 solin 
 |-  ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( a R b \/ a = b \/ b R a ) )
80 5 7 10 79 syl12anc 
 |-  ( ph -> ( a R b \/ a = b \/ b R a ) )
81 28 57 78 80 mpjao3dan 
 |-  ( ph -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) )
82 r19.26 
 |-  ( 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 ) ) ) )
83 9 12 82 sylanbrc 
 |-  ( ph -> A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) )
84 5 7 10 3jca 
 |-  ( ph -> ( R Or A /\ a e. A /\ b e. A ) )
85 anim12 
 |-  ( ( ( 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 ) ) ) )
86 eqtr 
 |-  ( ( ( P ` c ) = ( X ` c ) /\ ( X ` c ) = ( Q ` c ) ) -> ( P ` c ) = ( Q ` c ) )
87 85 86 syl6 
 |-  ( ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) )
88 87 ralimi 
 |-  ( 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 ) ) )
89 simpl1 
 |-  ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> R Or A )
90 simpr 
 |-  ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> c e. A )
91 simpl2 
 |-  ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> a e. A )
92 simpl3 
 |-  ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> b e. A )
93 soltmin 
 |-  ( ( 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 ) ) )
94 89 90 91 92 93 syl13anc 
 |-  ( ( ( 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 ) ) )
95 94 biimpd 
 |-  ( ( ( 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 imim1d 
 |-  ( ( ( 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 ) ) ) )
97 96 ralimdva 
 |-  ( ( 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 ) ) ) )
98 84 88 97 syl2im 
 |-  ( 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 ) ) ) )
99 83 98 mpd 
 |-  ( ph -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) )
100 fveq2 
 |-  ( d = if ( a R b , a , b ) -> ( P ` d ) = ( P ` if ( a R b , a , b ) ) )
101 fveq2 
 |-  ( d = if ( a R b , a , b ) -> ( Q ` d ) = ( Q ` if ( a R b , a , b ) ) )
102 100 101 breq12d 
 |-  ( 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 ) ) ) )
103 breq2 
 |-  ( d = if ( a R b , a , b ) -> ( c R d <-> c R if ( a R b , a , b ) ) )
104 103 imbi1d 
 |-  ( 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 ) ) ) )
105 104 ralbidv 
 |-  ( 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 ) ) ) )
106 102 105 anbi12d 
 |-  ( 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 ) ) ) ) )
107 106 rspcev 
 |-  ( ( 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 ) ) ) )
108 13 81 99 107 syl12anc 
 |-  ( ph -> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) )
109 1 wemaplem1 
 |-  ( ( 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 ) ) ) ) )
110 2 4 109 syl2anc 
 |-  ( ph -> ( P T Q <-> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) )
111 108 110 mpbird 
 |-  ( ph -> P T Q )