Metamath Proof Explorer

Theorem fpwwe2lem9

Description: Lemma for fpwwe2 . Given two well-orders <. X , R >. and <. Y , S >. of parts of A , one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
fpwwe2.2 
|- ( ph -> A e. V )
fpwwe2.3 
|- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
fpwwe2lem9.4 
|- ( ph -> X W R )
fpwwe2lem9.6 
|- ( ph -> Y W S )
Assertion fpwwe2lem9 
|- ( ph -> ( ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) \/ ( Y C_ X /\ S = ( R i^i ( X X. Y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
2 fpwwe2.2 
 |-  ( ph -> A e. V )
3 fpwwe2.3 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
4 fpwwe2lem9.4 
 |-  ( ph -> X W R )
5 fpwwe2lem9.6 
 |-  ( ph -> Y W S )
6 eqid 
 |-  OrdIso ( R , X ) = OrdIso ( R , X )
7 6 oicl 
 |-  Ord dom OrdIso ( R , X )
8 eqid 
 |-  OrdIso ( S , Y ) = OrdIso ( S , Y )
9 8 oicl 
 |-  Ord dom OrdIso ( S , Y )
10 ordtri2or2 
 |-  ( ( Ord dom OrdIso ( R , X ) /\ Ord dom OrdIso ( S , Y ) ) -> ( dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) \/ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) )
11 7 9 10 mp2an 
 |-  ( dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) \/ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) )
12 2 adantr 
 |-  ( ( ph /\ dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) ) -> A e. V )
13 3 adantlr 
 |-  ( ( ( ph /\ dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
14 4 adantr 
 |-  ( ( ph /\ dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) ) -> X W R )
15 5 adantr 
 |-  ( ( ph /\ dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) ) -> Y W S )
16 simpr 
 |-  ( ( ph /\ dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) ) -> dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) )
17 1 12 13 14 15 6 8 16 fpwwe2lem8 
 |-  ( ( ph /\ dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) ) -> ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) )
18 17 ex 
 |-  ( ph -> ( dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) -> ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) ) )
19 2 adantr 
 |-  ( ( ph /\ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) -> A e. V )
20 3 adantlr 
 |-  ( ( ( ph /\ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
21 5 adantr 
 |-  ( ( ph /\ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) -> Y W S )
22 4 adantr 
 |-  ( ( ph /\ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) -> X W R )
23 simpr 
 |-  ( ( ph /\ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) -> dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) )
24 1 19 20 21 22 8 6 23 fpwwe2lem8 
 |-  ( ( ph /\ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) -> ( Y C_ X /\ S = ( R i^i ( X X. Y ) ) ) )
25 24 ex 
 |-  ( ph -> ( dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) -> ( Y C_ X /\ S = ( R i^i ( X X. Y ) ) ) ) )
26 18 25 orim12d 
 |-  ( ph -> ( ( dom OrdIso ( R , X ) C_ dom OrdIso ( S , Y ) \/ dom OrdIso ( S , Y ) C_ dom OrdIso ( R , X ) ) -> ( ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) \/ ( Y C_ X /\ S = ( R i^i ( X X. Y ) ) ) ) ) )
27 11 26 mpi 
 |-  ( ph -> ( ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) \/ ( Y C_ X /\ S = ( R i^i ( X X. Y ) ) ) ) )