Theorem cofon1

Description: Cofinality theorem for ordinals. If A is cofinal with B and the upper bound of A dominates B , then their upper bounds are equal. Compare with cofcut1 for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Hypotheses	cofon1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 On )
	cofon1.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
	cofon1.3	⊢ ( 𝜑 → 𝐵 ⊆ ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } )
Assertion	cofon1	⊢ ( 𝜑 → ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } = ∩ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } )

Proof

Step	Hyp	Ref	Expression
1		cofon1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 On )
2		cofon1.2	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
3		cofon1.3	⊢ ( 𝜑 → 𝐵 ⊆ ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } )
4		sseq2	⊢ ( 𝑤 = 𝑧 → ( 𝐵 ⊆ 𝑤 ↔ 𝐵 ⊆ 𝑧 ) )
5	4	cbvrabv	⊢ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } = { 𝑧 ∈ On ∣ 𝐵 ⊆ 𝑧 }
6		sseq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦 ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ↔ ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 ) )
8	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
9		simprr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → 𝑎 ∈ 𝐴 )
10	7 8 9	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 )
11		sseq2	⊢ ( 𝑦 = 𝑏 → ( 𝑎 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑏 ) )
12	11	cbvrexvw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦 ↔ ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 )
13	10 12	sylib	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 )
14		simprl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → 𝐵 ⊆ 𝑧 )
15	14	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝑧 )
16	1	elpwid	⊢ ( 𝜑 → 𝐴 ⊆ On )
17	16	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ⊆ On )
18		simplrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐴 )
19	17 18	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ On )
20		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑧 ∈ On )
21		ontr2	⊢ ( ( 𝑎 ∈ On ∧ 𝑧 ∈ On ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑧 ) → 𝑎 ∈ 𝑧 ) )
22	19 20 21	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑧 ) → 𝑎 ∈ 𝑧 ) )
23	15 22	mpan2d	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑧 ) )
24	23	rexlimdva	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → ( ∃ 𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑧 ) )
25	13 24	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ( 𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴 ) ) → 𝑎 ∈ 𝑧 )
26	25	expr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ 𝐵 ⊆ 𝑧 ) → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑧 ) )
27	26	ssrdv	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ 𝐵 ⊆ 𝑧 ) → 𝐴 ⊆ 𝑧 )
28	27	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝐵 ⊆ 𝑧 → 𝐴 ⊆ 𝑧 ) )
29	28	ss2rabdv	⊢ ( 𝜑 → { 𝑧 ∈ On ∣ 𝐵 ⊆ 𝑧 } ⊆ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } )
30	5 29	eqsstrid	⊢ ( 𝜑 → { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } ⊆ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } )
31		intss	⊢ ( { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } ⊆ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } → ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ⊆ ∩ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } )
32	30 31	syl	⊢ ( 𝜑 → ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ⊆ ∩ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } )
33		sseq2	⊢ ( 𝑤 = ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } → ( 𝐵 ⊆ 𝑤 ↔ 𝐵 ⊆ ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ) )
34		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
35	16 34	syl	⊢ ( 𝜑 → Ord ∪ 𝐴 )
36		ordsuc	⊢ ( Ord ∪ 𝐴 ↔ Ord suc ∪ 𝐴 )
37	35 36	sylib	⊢ ( 𝜑 → Ord suc ∪ 𝐴 )
38	1	uniexd	⊢ ( 𝜑 → ∪ 𝐴 ∈ V )
39		sucexg	⊢ ( ∪ 𝐴 ∈ V → suc ∪ 𝐴 ∈ V )
40	38 39	syl	⊢ ( 𝜑 → suc ∪ 𝐴 ∈ V )
41		elong	⊢ ( suc ∪ 𝐴 ∈ V → ( suc ∪ 𝐴 ∈ On ↔ Ord suc ∪ 𝐴 ) )
42	40 41	syl	⊢ ( 𝜑 → ( suc ∪ 𝐴 ∈ On ↔ Ord suc ∪ 𝐴 ) )
43	37 42	mpbird	⊢ ( 𝜑 → suc ∪ 𝐴 ∈ On )
44		onsucuni	⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )
45	16 44	syl	⊢ ( 𝜑 → 𝐴 ⊆ suc ∪ 𝐴 )
46		sseq2	⊢ ( 𝑧 = suc ∪ 𝐴 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ suc ∪ 𝐴 ) )
47	46	rspcev	⊢ ( ( suc ∪ 𝐴 ∈ On ∧ 𝐴 ⊆ suc ∪ 𝐴 ) → ∃ 𝑧 ∈ On 𝐴 ⊆ 𝑧 )
48	43 45 47	syl2anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ On 𝐴 ⊆ 𝑧 )
49		onintrab2	⊢ ( ∃ 𝑧 ∈ On 𝐴 ⊆ 𝑧 ↔ ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ∈ On )
50	48 49	sylib	⊢ ( 𝜑 → ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ∈ On )
51	33 50 3	elrabd	⊢ ( 𝜑 → ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ∈ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } )
52		intss1	⊢ ( ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } ∈ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } → ∩ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } ⊆ ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } )
53	51 52	syl	⊢ ( 𝜑 → ∩ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } ⊆ ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } )
54	32 53	eqssd	⊢ ( 𝜑 → ∩ { 𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧 } = ∩ { 𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤 } )