Theorem cofonr

Description: Inverse cofinality law for ordinals. Contrast with cofcutr for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Hypotheses	cofonr.1	⊢ ( 𝜑 → 𝐴 ∈ On )
	cofonr.2	⊢ ( 𝜑 → 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } )
Assertion	cofonr	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		cofonr.1	⊢ ( 𝜑 → 𝐴 ∈ On )
2		cofonr.2	⊢ ( 𝜑 → 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } )
3		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
4	1 3	syl	⊢ ( 𝜑 → 𝐴 ⊆ On )
5	4	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
6		eloni	⊢ ( 𝑦 ∈ On → Ord 𝑦 )
7		ordirr	⊢ ( Ord 𝑦 → ¬ 𝑦 ∈ 𝑦 )
8	5 6 7	3syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ 𝑦 ∈ 𝑦 )
9	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } )
10	9	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } )
11	5	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑦 ∈ On )
12		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑋 ⊆ 𝑦 )
13		sseq2	⊢ ( 𝑥 = 𝑦 → ( 𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ 𝑦 ) )
14	13	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } ↔ ( 𝑦 ∈ On ∧ 𝑋 ⊆ 𝑦 ) )
15	11 12 14	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } )
16		intss1	⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } → ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } ⊆ 𝑦 )
17	15 16	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } ⊆ 𝑦 )
18	10 17	eqsstrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝐴 ⊆ 𝑦 )
19		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑦 ∈ 𝐴 )
20	18 19	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑋 ⊆ 𝑦 ) → 𝑦 ∈ 𝑦 )
21	8 20	mtand	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ 𝑋 ⊆ 𝑦 )
22		dfss3	⊢ ( 𝑋 ⊆ 𝑦 ↔ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ 𝑦 )
23	21 22	sylnib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ 𝑦 )
24	2 1	eqeltrrd	⊢ ( 𝜑 → ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } ∈ On )
25		onintrab2	⊢ ( ∃ 𝑥 ∈ On 𝑋 ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥 } ∈ On )
26	24 25	sylibr	⊢ ( 𝜑 → ∃ 𝑥 ∈ On 𝑋 ⊆ 𝑥 )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ On 𝑋 ⊆ 𝑥 )
28		onss	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
29	28	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ On ) → 𝑥 ⊆ On )
30		sstr	⊢ ( ( 𝑋 ⊆ 𝑥 ∧ 𝑥 ⊆ On ) → 𝑋 ⊆ On )
31	30	expcom	⊢ ( 𝑥 ⊆ On → ( 𝑋 ⊆ 𝑥 → 𝑋 ⊆ On ) )
32	29 31	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ On ) → ( 𝑋 ⊆ 𝑥 → 𝑋 ⊆ On ) )
33	32	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ On 𝑋 ⊆ 𝑥 → 𝑋 ⊆ On ) )
34	27 33	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑋 ⊆ On )
35	34	sselda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ On )
36		ontri1	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑦 ) )
37	5 35 36	syl2an2r	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑦 ) )
38	37	rexbidva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 ↔ ∃ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ 𝑦 ) )
39		rexnal	⊢ ( ∃ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ 𝑦 ↔ ¬ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ 𝑦 )
40	38 39	bitrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 ↔ ¬ ∀ 𝑧 ∈ 𝑋 𝑧 ∈ 𝑦 ) )
41	23 40	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 )
42	41	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 )