Metamath Proof Explorer

Theorem fpwwe2lem8

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. (The O C_ P hypothesis is in order to break the symmetry of X and Y .) (Contributed by Mario Carneiro, 15-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (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 )
fpwwe2lem8.x 
|- ( ph -> X W R )
fpwwe2lem8.y 
|- ( ph -> Y W S )
fpwwe2lem8.m 
|- M = OrdIso ( R , X )
fpwwe2lem8.n 
|- N = OrdIso ( S , Y )
fpwwe2lem8.s 
|- ( ph -> dom M C_ dom N )
Assertion fpwwe2lem8 
|- ( ph -> ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) )

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 fpwwe2lem8.x 
 |-  ( ph -> X W R )
5 fpwwe2lem8.y 
 |-  ( ph -> Y W S )
6 fpwwe2lem8.m 
 |-  M = OrdIso ( R , X )
7 fpwwe2lem8.n 
 |-  N = OrdIso ( S , Y )
8 fpwwe2lem8.s 
 |-  ( ph -> dom M C_ dom N )
9 1 relopabiv 
 |-  Rel W
10 9 brrelex1i 
 |-  ( X W R -> X e. _V )
11 4 10 syl 
 |-  ( ph -> X e. _V )
12 1 2 fpwwe2lem2 
 |-  ( ph -> ( X W 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 ) ) ) )
13 4 12 mpbid 
 |-  ( ph -> ( ( 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 ) ) )
14 13 simprld 
 |-  ( ph -> R We X )
15 6 oiiso 
 |-  ( ( X e. _V /\ R We X ) -> M Isom _E , R ( dom M , X ) )
16 11 14 15 syl2anc 
 |-  ( ph -> M Isom _E , R ( dom M , X ) )
17 isof1o 
 |-  ( M Isom _E , R ( dom M , X ) -> M : dom M -1-1-onto-> X )
18 16 17 syl 
 |-  ( ph -> M : dom M -1-1-onto-> X )
19 f1ofo 
 |-  ( M : dom M -1-1-onto-> X -> M : dom M -onto-> X )
20 forn 
 |-  ( M : dom M -onto-> X -> ran M = X )
21 18 19 20 3syl 
 |-  ( ph -> ran M = X )
22 1 2 3 4 5 6 7 8 fpwwe2lem7 
 |-  ( ph -> M = ( N |` dom M ) )
23 22 rneqd 
 |-  ( ph -> ran M = ran ( N |` dom M ) )
24 21 23 eqtr3d 
 |-  ( ph -> X = ran ( N |` dom M ) )
25 df-ima 
 |-  ( N " dom M ) = ran ( N |` dom M )
26 24 25 eqtr4di 
 |-  ( ph -> X = ( N " dom M ) )
27 imassrn 
 |-  ( N " dom M ) C_ ran N
28 9 brrelex1i 
 |-  ( Y W S -> Y e. _V )
29 5 28 syl 
 |-  ( ph -> Y e. _V )
30 1 2 fpwwe2lem2 
 |-  ( ph -> ( Y W S <-> ( ( Y C_ A /\ S C_ ( Y X. Y ) ) /\ ( S We Y /\ A. y e. Y [. ( `' S " { y } ) / u ]. ( u F ( S i^i ( u X. u ) ) ) = y ) ) ) )
31 5 30 mpbid 
 |-  ( ph -> ( ( Y C_ A /\ S C_ ( Y X. Y ) ) /\ ( S We Y /\ A. y e. Y [. ( `' S " { y } ) / u ]. ( u F ( S i^i ( u X. u ) ) ) = y ) ) )
32 31 simprld 
 |-  ( ph -> S We Y )
33 7 oiiso 
 |-  ( ( Y e. _V /\ S We Y ) -> N Isom _E , S ( dom N , Y ) )
34 29 32 33 syl2anc 
 |-  ( ph -> N Isom _E , S ( dom N , Y ) )
35 isof1o 
 |-  ( N Isom _E , S ( dom N , Y ) -> N : dom N -1-1-onto-> Y )
36 34 35 syl 
 |-  ( ph -> N : dom N -1-1-onto-> Y )
37 f1ofo 
 |-  ( N : dom N -1-1-onto-> Y -> N : dom N -onto-> Y )
38 forn 
 |-  ( N : dom N -onto-> Y -> ran N = Y )
39 36 37 38 3syl 
 |-  ( ph -> ran N = Y )
40 27 39 sseqtrid 
 |-  ( ph -> ( N " dom M ) C_ Y )
41 26 40 eqsstrd 
 |-  ( ph -> X C_ Y )
42 13 simplrd 
 |-  ( ph -> R C_ ( X X. X ) )
43 relxp 
 |-  Rel ( X X. X )
44 relss 
 |-  ( R C_ ( X X. X ) -> ( Rel ( X X. X ) -> Rel R ) )
45 42 43 44 mpisyl 
 |-  ( ph -> Rel R )
46 relinxp 
 |-  Rel ( S i^i ( Y X. X ) )
47 45 46 jctir 
 |-  ( ph -> ( Rel R /\ Rel ( S i^i ( Y X. X ) ) ) )
48 42 ssbrd 
 |-  ( ph -> ( x R y -> x ( X X. X ) y ) )
49 brxp 
 |-  ( x ( X X. X ) y <-> ( x e. X /\ y e. X ) )
50 48 49 syl6ib 
 |-  ( ph -> ( x R y -> ( x e. X /\ y e. X ) ) )
51 brinxp2 
 |-  ( x ( S i^i ( Y X. X ) ) y <-> ( ( x e. Y /\ y e. X ) /\ x S y ) )
52 isocnv 
 |-  ( N Isom _E , S ( dom N , Y ) -> `' N Isom S , _E ( Y , dom N ) )
53 34 52 syl 
 |-  ( ph -> `' N Isom S , _E ( Y , dom N ) )
54 53 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' N Isom S , _E ( Y , dom N ) )
55 isof1o 
 |-  ( `' N Isom S , _E ( Y , dom N ) -> `' N : Y -1-1-onto-> dom N )
56 f1ofn 
 |-  ( `' N : Y -1-1-onto-> dom N -> `' N Fn Y )
57 54 55 56 3syl 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' N Fn Y )
58 simprll 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x e. Y )
59 simprr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x S y )
60 41 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> X C_ Y )
61 simprlr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> y e. X )
62 60 61 sseldd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> y e. Y )
63 isorel 
 |-  ( ( `' N Isom S , _E ( Y , dom N ) /\ ( x e. Y /\ y e. Y ) ) -> ( x S y <-> ( `' N ` x ) _E ( `' N ` y ) ) )
64 54 58 62 63 syl12anc 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( x S y <-> ( `' N ` x ) _E ( `' N ` y ) ) )
65 59 64 mpbid 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` x ) _E ( `' N ` y ) )
66 fvex 
 |-  ( `' N ` y ) e. _V
67 66 epeli 
 |-  ( ( `' N ` x ) _E ( `' N ` y ) <-> ( `' N ` x ) e. ( `' N ` y ) )
68 65 67 sylib 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` x ) e. ( `' N ` y ) )
69 22 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> M = ( N |` dom M ) )
70 69 cnveqd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' M = `' ( N |` dom M ) )
71 fnfun 
 |-  ( `' N Fn Y -> Fun `' N )
72 funcnvres 
 |-  ( Fun `' N -> `' ( N |` dom M ) = ( `' N |` ( N " dom M ) ) )
73 57 71 72 3syl 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' ( N |` dom M ) = ( `' N |` ( N " dom M ) ) )
74 70 73 eqtrd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' M = ( `' N |` ( N " dom M ) ) )
75 74 fveq1d 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' M ` y ) = ( ( `' N |` ( N " dom M ) ) ` y ) )
76 26 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> X = ( N " dom M ) )
77 61 76 eleqtrd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> y e. ( N " dom M ) )
78 77 fvresd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( ( `' N |` ( N " dom M ) ) ` y ) = ( `' N ` y ) )
79 75 78 eqtrd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' M ` y ) = ( `' N ` y ) )
80 isocnv 
 |-  ( M Isom _E , R ( dom M , X ) -> `' M Isom R , _E ( X , dom M ) )
81 16 80 syl 
 |-  ( ph -> `' M Isom R , _E ( X , dom M ) )
82 isof1o 
 |-  ( `' M Isom R , _E ( X , dom M ) -> `' M : X -1-1-onto-> dom M )
83 f1of 
 |-  ( `' M : X -1-1-onto-> dom M -> `' M : X --> dom M )
84 81 82 83 3syl 
 |-  ( ph -> `' M : X --> dom M )
85 84 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' M : X --> dom M )
86 85 61 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' M ` y ) e. dom M )
87 79 86 eqeltrrd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` y ) e. dom M )
88 6 oicl 
 |-  Ord dom M
89 ordtr1 
 |-  ( Ord dom M -> ( ( ( `' N ` x ) e. ( `' N ` y ) /\ ( `' N ` y ) e. dom M ) -> ( `' N ` x ) e. dom M ) )
90 88 89 ax-mp 
 |-  ( ( ( `' N ` x ) e. ( `' N ` y ) /\ ( `' N ` y ) e. dom M ) -> ( `' N ` x ) e. dom M )
91 68 87 90 syl2anc 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` x ) e. dom M )
92 57 58 91 elpreimad 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x e. ( `' `' N " dom M ) )
93 imacnvcnv 
 |-  ( `' `' N " dom M ) = ( N " dom M )
94 76 93 eqtr4di 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> X = ( `' `' N " dom M ) )
95 92 94 eleqtrrd 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x e. X )
96 95 61 jca 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( x e. X /\ y e. X ) )
97 96 ex 
 |-  ( ph -> ( ( ( x e. Y /\ y e. X ) /\ x S y ) -> ( x e. X /\ y e. X ) ) )
98 51 97 syl5bi 
 |-  ( ph -> ( x ( S i^i ( Y X. X ) ) y -> ( x e. X /\ y e. X ) ) )
99 22 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> M = ( N |` dom M ) )
100 99 cnveqd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> `' M = `' ( N |` dom M ) )
101 100 fveq1d 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( `' M ` x ) = ( `' ( N |` dom M ) ` x ) )
102 100 fveq1d 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( `' M ` y ) = ( `' ( N |` dom M ) ` y ) )
103 101 102 breq12d 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( `' M ` x ) _E ( `' M ` y ) <-> ( `' ( N |` dom M ) ` x ) _E ( `' ( N |` dom M ) ` y ) ) )
104 isorel 
 |-  ( ( `' M Isom R , _E ( X , dom M ) /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> ( `' M ` x ) _E ( `' M ` y ) ) )
105 81 104 sylan 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> ( `' M ` x ) _E ( `' M ` y ) ) )
106 eqidd 
 |-  ( ph -> ( N " dom M ) = ( N " dom M ) )
107 isores3 
 |-  ( ( N Isom _E , S ( dom N , Y ) /\ dom M C_ dom N /\ ( N " dom M ) = ( N " dom M ) ) -> ( N |` dom M ) Isom _E , S ( dom M , ( N " dom M ) ) )
108 34 8 106 107 syl3anc 
 |-  ( ph -> ( N |` dom M ) Isom _E , S ( dom M , ( N " dom M ) ) )
109 isocnv 
 |-  ( ( N |` dom M ) Isom _E , S ( dom M , ( N " dom M ) ) -> `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) )
110 108 109 syl 
 |-  ( ph -> `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) )
111 110 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) )
112 simprl 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. X )
113 26 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> X = ( N " dom M ) )
114 112 113 eleqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. ( N " dom M ) )
115 simprr 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> y e. X )
116 115 113 eleqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> y e. ( N " dom M ) )
117 isorel 
 |-  ( ( `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) /\ ( x e. ( N " dom M ) /\ y e. ( N " dom M ) ) ) -> ( x S y <-> ( `' ( N |` dom M ) ` x ) _E ( `' ( N |` dom M ) ` y ) ) )
118 111 114 116 117 syl12anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x S y <-> ( `' ( N |` dom M ) ` x ) _E ( `' ( N |` dom M ) ` y ) ) )
119 103 105 118 3bitr4d 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> x S y ) )
120 41 sselda 
 |-  ( ( ph /\ x e. X ) -> x e. Y )
121 120 adantrr 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. Y )
122 121 115 jca 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x e. Y /\ y e. X ) )
123 122 biantrurd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x S y <-> ( ( x e. Y /\ y e. X ) /\ x S y ) ) )
124 123 51 bitr4di 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x S y <-> x ( S i^i ( Y X. X ) ) y ) )
125 119 124 bitrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> x ( S i^i ( Y X. X ) ) y ) )
126 125 ex 
 |-  ( ph -> ( ( x e. X /\ y e. X ) -> ( x R y <-> x ( S i^i ( Y X. X ) ) y ) ) )
127 50 98 126 pm5.21ndd 
 |-  ( ph -> ( x R y <-> x ( S i^i ( Y X. X ) ) y ) )
128 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
129 df-br 
 |-  ( x ( S i^i ( Y X. X ) ) y <-> <. x , y >. e. ( S i^i ( Y X. X ) ) )
130 127 128 129 3bitr3g 
 |-  ( ph -> ( <. x , y >. e. R <-> <. x , y >. e. ( S i^i ( Y X. X ) ) ) )
131 130 eqrelrdv2 
 |-  ( ( ( Rel R /\ Rel ( S i^i ( Y X. X ) ) ) /\ ph ) -> R = ( S i^i ( Y X. X ) ) )
132 47 131 mpancom 
 |-  ( ph -> R = ( S i^i ( Y X. X ) ) )
133 41 132 jca 
 |-  ( ph -> ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) )