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 A r x × x r We x y x [˙ r -1 y / u]˙ u F r u × u = y
fpwwe2.2 φ A V
fpwwe2.3 φ x A r x × x r We x x F r A
fpwwe2lem8.x φ X W R
fpwwe2lem8.y φ Y W S
fpwwe2lem8.m M = OrdIso R X
fpwwe2lem8.n N = OrdIso S Y
fpwwe2lem8.s φ dom M dom N
Assertion fpwwe2lem8 φ X Y R = S Y × X

Proof

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