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 ∈ B x ⊆ y
cofon2.4 ⊢ φ → ∀ z ∈ B ∃ w ∈ A z ⊆ 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 ∈ B x ⊆ y
4 cofon2.4 ⊢ φ → ∀ z ∈ B ∃ w ∈ A z ⊆ w
5 sseq1 ⊢ z = b → z ⊆ w ↔ b ⊆ w
6 5 rexbidv ⊢ z = b → ∃ w ∈ A z ⊆ w ↔ ∃ w ∈ A b ⊆ w
7 4 adantr ⊢ φ ∧ b ∈ B → ∀ z ∈ B ∃ w ∈ A z ⊆ w
8 simpr ⊢ φ ∧ b ∈ B → b ∈ B
9 6 7 8 rspcdva ⊢ φ ∧ b ∈ B → ∃ w ∈ A b ⊆ w
10 sseq2 ⊢ w = c → b ⊆ w ↔ b ⊆ c
11 10 cbvrexvw ⊢ ∃ w ∈ A b ⊆ w ↔ ∃ c ∈ A b ⊆ c
12 9 11 sylib ⊢ φ ∧ b ∈ B → ∃ c ∈ A b ⊆ 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 ∈ On A ⊆ a
34 29 31 33 syl2anc ⊢ φ → ∃ a ∈ On A ⊆ a
35 onintrab2 ⊢ ∃ a ∈ On A ⊆ 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 ∈ A b ⊆ 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