Metamath Proof Explorer

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 ⊢φ→A∈𝒫On
cofon2.2 ⊢φ→B∈𝒫On
cofon2.3 ⊢φ→∀x∈A∃y∈Bx⊆y
cofon2.4 ⊢φ→∀z∈B∃w∈Az⊆w
Assertion cofon2 ⊢φ→⋂a∈On|A⊆a=⋂b∈On|B⊆b

Proof

Step Hyp Ref Expression
1 cofon2.1 ⊢φ→A∈𝒫On
2 cofon2.2 ⊢φ→B∈𝒫On
3 cofon2.3 ⊢φ→∀x∈A∃y∈Bx⊆y
4 cofon2.4 ⊢φ→∀z∈B∃w∈Az⊆w
5 sseq1 ⊢z=b→z⊆w↔b⊆w
6 5 rexbidv ⊢z=b→∃w∈Az⊆w↔∃w∈Ab⊆w
7 4 adantr ⊢φ∧b∈B→∀z∈B∃w∈Az⊆w
8 simpr ⊢φ∧b∈B→b∈B
9 6 7 8 rspcdva ⊢φ∧b∈B→∃w∈Ab⊆w
10 sseq2 ⊢w=c→b⊆w↔b⊆c
11 10 cbvrexvw ⊢∃w∈Ab⊆w↔∃c∈Ab⊆c
12 9 11 sylib ⊢φ∧b∈B→∃c∈Ab⊆c
13 ssintub ⊢A⊆⋂a∈On|A⊆a
14 13 a1i ⊢φ∧b∈B→A⊆⋂a∈On|A⊆a
15 14 sselda ⊢φ∧b∈B∧c∈A→c∈⋂a∈On|A⊆a
16 2 elpwid ⊢φ→B⊆On
17 16 ad2antrr ⊢φ∧b∈B∧c∈A→B⊆On
18 simplr ⊢φ∧b∈B∧c∈A→b∈B
19 17 18 sseldd ⊢φ∧b∈B∧c∈A→b∈On
20 1 elpwid ⊢φ→A⊆On
21 ssorduni ⊢A⊆On→Ord⁡⋃A
22 20 21 syl ⊢φ→Ord⁡⋃A
23 ordsuc ⊢Ord⁡⋃A↔Ord⁡suc⁡⋃A
24 22 23 sylib ⊢φ→Ord⁡suc⁡⋃A
25 1 uniexd ⊢φ→⋃A∈V
26 sucexg ⊢⋃A∈V→suc⁡⋃A∈V
27 elong ⊢suc⁡⋃A∈V→suc⁡⋃A∈On↔Ord⁡suc⁡⋃A
28 25 26 27 3syl ⊢φ→suc⁡⋃A∈On↔Ord⁡suc⁡⋃A
29 24 28 mpbird ⊢φ→suc⁡⋃A∈On
30 onsucuni ⊢A⊆On→A⊆suc⁡⋃A
31 20 30 syl ⊢φ→A⊆suc⁡⋃A
32 sseq2 ⊢a=suc⁡⋃A→A⊆a↔A⊆suc⁡⋃A
33 32 rspcev ⊢suc⁡⋃A∈On∧A⊆suc⁡⋃A→∃a∈OnA⊆a
34 29 31 33 syl2anc ⊢φ→∃a∈OnA⊆a
35 onintrab2 ⊢∃a∈OnA⊆a↔⋂a∈On|A⊆a∈On
36 34 35 sylib ⊢φ→⋂a∈On|A⊆a∈On
37 36 ad2antrr ⊢φ∧b∈B∧c∈A→⋂a∈On|A⊆a∈On
38 ontr2 ⊢b∈On∧⋂a∈On|A⊆a∈On→b⊆c∧c∈⋂a∈On|A⊆a→b∈⋂a∈On|A⊆a
39 19 37 38 syl2anc ⊢φ∧b∈B∧c∈A→b⊆c∧c∈⋂a∈On|A⊆a→b∈⋂a∈On|A⊆a
40 15 39 mpan2d ⊢φ∧b∈B∧c∈A→b⊆c→b∈⋂a∈On|A⊆a
41 40 rexlimdva ⊢φ∧b∈B→∃c∈Ab⊆c→b∈⋂a∈On|A⊆a
42 12 41 mpd ⊢φ∧b∈B→b∈⋂a∈On|A⊆a
43 42 ex ⊢φ→b∈B→b∈⋂a∈On|A⊆a
44 43 ssrdv ⊢φ→B⊆⋂a∈On|A⊆a
45 1 3 44 cofon1 ⊢φ→⋂a∈On|A⊆a=⋂b∈On|B⊆b