This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wemaplem3

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 )
wemaplem3.px 
|- ( ph -> P T X )
wemaplem3.xq 
|- ( ph -> X T Q )
Assertion wemaplem3 
|- ( 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 wemaplem3.px 
 |-  ( ph -> P T X )
8 wemaplem3.xq 
 |-  ( ph -> X T Q )
9 1 wemaplem1 
 |-  ( ( P e. ( B ^m A ) /\ X e. ( B ^m A ) ) -> ( P T X <-> E. a e. A ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) )
10 2 3 9 syl2anc 
 |-  ( ph -> ( P T X <-> E. a e. A ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) )
11 7 10 mpbid 
 |-  ( ph -> E. a e. A ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) )
12 1 wemaplem1 
 |-  ( ( X e. ( B ^m A ) /\ Q e. ( B ^m A ) ) -> ( X T Q <-> E. b e. A ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) )
13 3 4 12 syl2anc 
 |-  ( ph -> ( X T Q <-> E. b e. A ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) )
14 8 13 mpbid 
 |-  ( ph -> E. b e. A ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) )
15 2 ad2antrr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> P e. ( B ^m A ) )
16 3 ad2antrr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> X e. ( B ^m A ) )
17 4 ad2antrr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> Q e. ( B ^m A ) )
18 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> R Or A )
19 6 ad2antrr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> S Po B )
20 simplrl 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> a e. A )
21 simp2rl 
 |-  ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> ( P ` a ) S ( X ` a ) )
22 21 3expa 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> ( P ` a ) S ( X ` a ) )
23 simprr 
 |-  ( ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) -> A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) )
24 23 ad2antlr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) )
25 simprl 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> b e. A )
26 simprrl 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> ( X ` b ) S ( Q ` b ) )
27 simprrr 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) )
28 1 15 16 17 18 19 20 22 24 25 26 27 wemaplem2 
 |-  ( ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) /\ ( b e. A /\ ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) ) -> P T Q )
29 28 rexlimdvaa 
 |-  ( ( ph /\ ( a e. A /\ ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) ) ) -> ( E. b e. A ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> P T Q ) )
30 29 rexlimdvaa 
 |-  ( ph -> ( E. a e. A ( ( P ` a ) S ( X ` a ) /\ A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) -> ( E. b e. A ( ( X ` b ) S ( Q ` b ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> P T Q ) ) )
31 11 14 30 mp2d 
 |-  ( ph -> P T Q )