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 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
fpwwe2.2 ( 𝜑𝐴𝑉 )
fpwwe2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
fpwwe2lem9.4 ( 𝜑𝑋 𝑊 𝑅 )
fpwwe2lem9.6 ( 𝜑𝑌 𝑊 𝑆 )
Assertion fpwwe2lem9 ( 𝜑 → ( ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌𝑋𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ( 𝜑𝐴𝑉 )
3 fpwwe2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2lem9.4 ( 𝜑𝑋 𝑊 𝑅 )
5 fpwwe2lem9.6 ( 𝜑𝑌 𝑊 𝑆 )
6 eqid OrdIso ( 𝑅 , 𝑋 ) = OrdIso ( 𝑅 , 𝑋 )
7 6 oicl Ord dom OrdIso ( 𝑅 , 𝑋 )
8 eqid OrdIso ( 𝑆 , 𝑌 ) = OrdIso ( 𝑆 , 𝑌 )
9 8 oicl Ord dom OrdIso ( 𝑆 , 𝑌 )
10 ordtri2or2 ( ( Ord dom OrdIso ( 𝑅 , 𝑋 ) ∧ Ord dom OrdIso ( 𝑆 , 𝑌 ) ) → ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ∨ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) )
11 7 9 10 mp2an ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ∨ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) )
12 2 adantr ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → 𝐴𝑉 )
13 3 adantlr ( ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
14 4 adantr ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → 𝑋 𝑊 𝑅 )
15 5 adantr ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → 𝑌 𝑊 𝑆 )
16 simpr ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) )
17 1 12 13 14 15 6 8 16 fpwwe2lem8 ( ( 𝜑 ∧ dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ) → ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )
18 17 ex ( 𝜑 → ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) → ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ) )
19 2 adantr ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → 𝐴𝑉 )
20 3 adantlr ( ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
21 5 adantr ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → 𝑌 𝑊 𝑆 )
22 4 adantr ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → 𝑋 𝑊 𝑅 )
23 simpr ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) )
24 1 19 20 21 22 8 6 23 fpwwe2lem8 ( ( 𝜑 ∧ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → ( 𝑌𝑋𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) )
25 24 ex ( 𝜑 → ( dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) → ( 𝑌𝑋𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) )
26 18 25 orim12d ( 𝜑 → ( ( dom OrdIso ( 𝑅 , 𝑋 ) ⊆ dom OrdIso ( 𝑆 , 𝑌 ) ∨ dom OrdIso ( 𝑆 , 𝑌 ) ⊆ dom OrdIso ( 𝑅 , 𝑋 ) ) → ( ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌𝑋𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) ) )
27 11 26 mpi ( 𝜑 → ( ( 𝑋𝑌𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌𝑋𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) )