# Metamath Proof Explorer

## Theorem fpwwe2lem10

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)

Ref Expression
Hypotheses fpwwe2.1
fpwwe2.2 ${⊢}{\phi }\to {A}\in \mathrm{V}$
fpwwe2.3 ${⊢}\left({\phi }\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
fpwwe2lem10.4 ${⊢}{\phi }\to {X}{W}{R}$
fpwwe2lem10.6 ${⊢}{\phi }\to {Y}{W}{S}$
Assertion fpwwe2lem10 ${⊢}{\phi }\to \left(\left({X}\subseteq {Y}\wedge {R}={S}\cap \left({Y}×{X}\right)\right)\vee \left({Y}\subseteq {X}\wedge {S}={R}\cap \left({X}×{Y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 fpwwe2.1
2 fpwwe2.2 ${⊢}{\phi }\to {A}\in \mathrm{V}$
3 fpwwe2.3 ${⊢}\left({\phi }\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
4 fpwwe2lem10.4 ${⊢}{\phi }\to {X}{W}{R}$
5 fpwwe2lem10.6 ${⊢}{\phi }\to {Y}{W}{S}$
6 eqid ${⊢}OrdIso\left({R},{X}\right)=OrdIso\left({R},{X}\right)$
7 6 oicl ${⊢}\mathrm{Ord}\mathrm{dom}OrdIso\left({R},{X}\right)$
8 eqid ${⊢}OrdIso\left({S},{Y}\right)=OrdIso\left({S},{Y}\right)$
9 8 oicl ${⊢}\mathrm{Ord}\mathrm{dom}OrdIso\left({S},{Y}\right)$
10 ordtri2or2 ${⊢}\left(\mathrm{Ord}\mathrm{dom}OrdIso\left({R},{X}\right)\wedge \mathrm{Ord}\mathrm{dom}OrdIso\left({S},{Y}\right)\right)\to \left(\mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\vee \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)$
11 7 9 10 mp2an ${⊢}\left(\mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\vee \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)$
12 2 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\right)\to {A}\in \mathrm{V}$
13 3 adantlr ${⊢}\left(\left({\phi }\wedge \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\right)\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
14 4 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\right)\to {X}{W}{R}$
15 5 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\right)\to {Y}{W}{S}$
16 simpr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\right)\to \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)$
17 1 12 13 14 15 6 8 16 fpwwe2lem9 ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\right)\to \left({X}\subseteq {Y}\wedge {R}={S}\cap \left({Y}×{X}\right)\right)$
18 17 ex ${⊢}{\phi }\to \left(\mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\to \left({X}\subseteq {Y}\wedge {R}={S}\cap \left({Y}×{X}\right)\right)\right)$
19 2 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\to {A}\in \mathrm{V}$
20 3 adantlr ${⊢}\left(\left({\phi }\wedge \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
21 5 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\to {Y}{W}{S}$
22 4 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\to {X}{W}{R}$
23 simpr ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\to \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)$
24 1 19 20 21 22 8 6 23 fpwwe2lem9 ${⊢}\left({\phi }\wedge \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\to \left({Y}\subseteq {X}\wedge {S}={R}\cap \left({X}×{Y}\right)\right)$
25 24 ex ${⊢}{\phi }\to \left(\mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\to \left({Y}\subseteq {X}\wedge {S}={R}\cap \left({X}×{Y}\right)\right)\right)$
26 18 25 orim12d ${⊢}{\phi }\to \left(\left(\mathrm{dom}OrdIso\left({R},{X}\right)\subseteq \mathrm{dom}OrdIso\left({S},{Y}\right)\vee \mathrm{dom}OrdIso\left({S},{Y}\right)\subseteq \mathrm{dom}OrdIso\left({R},{X}\right)\right)\to \left(\left({X}\subseteq {Y}\wedge {R}={S}\cap \left({Y}×{X}\right)\right)\vee \left({Y}\subseteq {X}\wedge {S}={R}\cap \left({X}×{Y}\right)\right)\right)\right)$
27 11 26 mpi ${⊢}{\phi }\to \left(\left({X}\subseteq {Y}\wedge {R}={S}\cap \left({Y}×{X}\right)\right)\vee \left({Y}\subseteq {X}\wedge {S}={R}\cap \left({X}×{Y}\right)\right)\right)$