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 )