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 ⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∨ ( 𝑌 ⊆ 𝑋 ∧ 𝑆 = ( 𝑅 ∩ ( 𝑋 × 𝑌 ) ) ) ) )