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 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
fpwwe2lem9.4 φ X W R
fpwwe2lem9.6 φ Y W S
Assertion fpwwe2lem9 φ X Y R = S Y × X Y X S = R X × Y

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 fpwwe2lem9.4 φ X W R
5 fpwwe2lem9.6 φ 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 dom OrdIso S Y dom OrdIso S Y dom OrdIso R X
11 7 9 10 mp2an dom OrdIso R X dom OrdIso S Y dom OrdIso S Y dom OrdIso R X
12 2 adantr φ dom OrdIso R X dom OrdIso S Y A V
13 3 adantlr φ dom OrdIso R X dom OrdIso S Y x A r x × x r We x x F r A
14 4 adantr φ dom OrdIso R X dom OrdIso S Y X W R
15 5 adantr φ dom OrdIso R X dom OrdIso S Y Y W S
16 simpr φ dom OrdIso R X dom OrdIso S Y dom OrdIso R X dom OrdIso S Y
17 1 12 13 14 15 6 8 16 fpwwe2lem8 φ dom OrdIso R X dom OrdIso S Y X Y R = S Y × X
18 17 ex φ dom OrdIso R X dom OrdIso S Y X Y R = S Y × X
19 2 adantr φ dom OrdIso S Y dom OrdIso R X A V
20 3 adantlr φ dom OrdIso S Y dom OrdIso R X x A r x × x r We x x F r A
21 5 adantr φ dom OrdIso S Y dom OrdIso R X Y W S
22 4 adantr φ dom OrdIso S Y dom OrdIso R X X W R
23 simpr φ dom OrdIso S Y dom OrdIso R X dom OrdIso S Y dom OrdIso R X
24 1 19 20 21 22 8 6 23 fpwwe2lem8 φ dom OrdIso S Y dom OrdIso R X Y X S = R X × Y
25 24 ex φ dom OrdIso S Y dom OrdIso R X Y X S = R X × Y
26 18 25 orim12d φ dom OrdIso R X dom OrdIso S Y dom OrdIso S Y dom OrdIso R X X Y R = S Y × X Y X S = R X × Y
27 11 26 mpi φ X Y R = S Y × X Y X S = R X × Y