Theorem cofon2

Description: Cofinality theorem for ordinals. If A and B are mutually cofinal, then their upper bounds agree. Compare cofcut2 for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cofon2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 On )
2		cofon2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 On )
3		cofon2.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
4		cofon2.4	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
5		sseq1	⊢ ( 𝑧 = 𝑏 → ( 𝑧 ⊆ 𝑤 ↔ 𝑏 ⊆ 𝑤 ) )
6	5	rexbidv	⊢ ( 𝑧 = 𝑏 → ( ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤 ) )
7	4	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
9	6 7 8	rspcdva	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤 )
10		sseq2	⊢ ( 𝑤 = 𝑐 → ( 𝑏 ⊆ 𝑤 ↔ 𝑏 ⊆ 𝑐 ) )
11	10	cbvrexvw	⊢ ( ∃ 𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤 ↔ ∃ 𝑐 ∈ 𝐴 𝑏 ⊆ 𝑐 )
12	9 11	sylib	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑐 ∈ 𝐴 𝑏 ⊆ 𝑐 )
13		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 }
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ⊆ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } )
15	14	sselda	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } )
16	2	elpwid	⊢ ( 𝜑 → 𝐵 ⊆ On )
17	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → 𝐵 ⊆ On )
18		simplr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑏 ∈ 𝐵 )
19	17 18	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → 𝑏 ∈ On )
20	1	elpwid	⊢ ( 𝜑 → 𝐴 ⊆ On )
21		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
22	20 21	syl	⊢ ( 𝜑 → Ord ∪ 𝐴 )
23		ordsuc	⊢ ( Ord ∪ 𝐴 ↔ Ord suc ∪ 𝐴 )
24	22 23	sylib	⊢ ( 𝜑 → Ord suc ∪ 𝐴 )
25	1	uniexd	⊢ ( 𝜑 → ∪ 𝐴 ∈ V )
26		sucexg	⊢ ( ∪ 𝐴 ∈ V → suc ∪ 𝐴 ∈ V )
27		elong	⊢ ( suc ∪ 𝐴 ∈ V → ( suc ∪ 𝐴 ∈ On ↔ Ord suc ∪ 𝐴 ) )
28	25 26 27	3syl	⊢ ( 𝜑 → ( suc ∪ 𝐴 ∈ On ↔ Ord suc ∪ 𝐴 ) )
29	24 28	mpbird	⊢ ( 𝜑 → suc ∪ 𝐴 ∈ On )
30		onsucuni	⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )
31	20 30	syl	⊢ ( 𝜑 → 𝐴 ⊆ suc ∪ 𝐴 )
32		sseq2	⊢ ( 𝑎 = suc ∪ 𝐴 → ( 𝐴 ⊆ 𝑎 ↔ 𝐴 ⊆ suc ∪ 𝐴 ) )
33	32	rspcev	⊢ ( ( suc ∪ 𝐴 ∈ On ∧ 𝐴 ⊆ suc ∪ 𝐴 ) → ∃ 𝑎 ∈ On 𝐴 ⊆ 𝑎 )
34	29 31 33	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ On 𝐴 ⊆ 𝑎 )
35		onintrab2	⊢ ( ∃ 𝑎 ∈ On 𝐴 ⊆ 𝑎 ↔ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ∈ On )
36	34 35	sylib	⊢ ( 𝜑 → ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ∈ On )
37	36	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ∈ On )
38		ontr2	⊢ ( ( 𝑏 ∈ On ∧ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ∈ On ) → ( ( 𝑏 ⊆ 𝑐 ∧ 𝑐 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) → 𝑏 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) )
39	19 37 38	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → ( ( 𝑏 ⊆ 𝑐 ∧ 𝑐 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) → 𝑏 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) )
40	15 39	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐴 ) → ( 𝑏 ⊆ 𝑐 → 𝑏 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) )
41	40	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ∃ 𝑐 ∈ 𝐴 𝑏 ⊆ 𝑐 → 𝑏 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) )
42	12 41	mpd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } )
43	42	ex	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } ) )
44	43	ssrdv	⊢ ( 𝜑 → 𝐵 ⊆ ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } )
45	1 3 44	cofon1	⊢ ( 𝜑 → ∩ { 𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎 } = ∩ { 𝑏 ∈ On ∣ 𝐵 ⊆ 𝑏 } )