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