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

Metamath Proof Explorer

Theorem fpwwe2lem9

Proof