Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 cofon1.1 ⊢ φ → A ∈ 𝒫 On
2 cofon1.2 ⊢ φ → ∀ x ∈ A ∃ y ∈ B x ⊆ y
3 cofon1.3 ⊢ φ → B ⊆ ⋂ z ∈ On | A ⊆ z
4 sseq2 ⊢ w = z → B ⊆ w ↔ B ⊆ z
5 4 cbvrabv ⊢ w ∈ On | B ⊆ w = z ∈ On | B ⊆ z
6 sseq1 ⊢ x = a → x ⊆ y ↔ a ⊆ y
7 6 rexbidv ⊢ x = a → ∃ y ∈ B x ⊆ y ↔ ∃ y ∈ B a ⊆ y
8 2 ad2antrr ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → ∀ x ∈ A ∃ y ∈ B x ⊆ y
9 simprr ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → a ∈ A
10 7 8 9 rspcdva ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → ∃ y ∈ B a ⊆ y
11 sseq2 ⊢ y = b → a ⊆ y ↔ a ⊆ b
12 11 cbvrexvw ⊢ ∃ y ∈ B a ⊆ y ↔ ∃ b ∈ B a ⊆ b
13 10 12 sylib ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → ∃ b ∈ B a ⊆ b
14 simprl ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → B ⊆ z
15 14 sselda ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → b ∈ z
16 1 elpwid ⊢ φ → A ⊆ On
17 16 ad3antrrr ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → A ⊆ On
18 simplrr ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → a ∈ A
19 17 18 sseldd ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → a ∈ On
20 simpllr ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → z ∈ On
21 ontr2 ⊢ a ∈ On ∧ z ∈ On → a ⊆ b ∧ b ∈ z → a ∈ z
22 19 20 21 syl2anc ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → a ⊆ b ∧ b ∈ z → a ∈ z
23 15 22 mpan2d ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A ∧ b ∈ B → a ⊆ b → a ∈ z
24 23 rexlimdva ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → ∃ b ∈ B a ⊆ b → a ∈ z
25 13 24 mpd ⊢ φ ∧ z ∈ On ∧ B ⊆ z ∧ a ∈ A → a ∈ z
26 25 expr ⊢ φ ∧ z ∈ On ∧ B ⊆ z → a ∈ A → a ∈ z
27 26 ssrdv ⊢ φ ∧ z ∈ On ∧ B ⊆ z → A ⊆ z
28 27 ex ⊢ φ ∧ z ∈ On → B ⊆ z → A ⊆ z
29 28 ss2rabdv ⊢ φ → z ∈ On | B ⊆ z ⊆ z ∈ On | A ⊆ z
30 5 29 eqsstrid ⊢ φ → w ∈ On | B ⊆ w ⊆ z ∈ On | A ⊆ z
31 intss ⊢ w ∈ On | B ⊆ w ⊆ z ∈ On | A ⊆ z → ⋂ z ∈ On | A ⊆ z ⊆ ⋂ w ∈ On | B ⊆ w
32 30 31 syl ⊢ φ → ⋂ z ∈ On | A ⊆ z ⊆ ⋂ w ∈ On | B ⊆ w
33 sseq2 ⊢ w = ⋂ z ∈ On | A ⊆ z → B ⊆ w ↔ B ⊆ ⋂ z ∈ On | A ⊆ z
34 ssorduni ⊢ A ⊆ On → Ord ⁡ ⋃ A
35 16 34 syl ⊢ φ → Ord ⁡ ⋃ A
36 ordsuc ⊢ Ord ⁡ ⋃ A ↔ Ord ⁡ suc ⁡ ⋃ A
37 35 36 sylib ⊢ φ → Ord ⁡ suc ⁡ ⋃ A
38 1 uniexd ⊢ φ → ⋃ A ∈ V
39 sucexg ⊢ ⋃ A ∈ V → suc ⁡ ⋃ A ∈ V
40 38 39 syl ⊢ φ → suc ⁡ ⋃ A ∈ V
41 elong ⊢ suc ⁡ ⋃ A ∈ V → suc ⁡ ⋃ A ∈ On ↔ Ord ⁡ suc ⁡ ⋃ A
42 40 41 syl ⊢ φ → suc ⁡ ⋃ A ∈ On ↔ Ord ⁡ suc ⁡ ⋃ A
43 37 42 mpbird ⊢ φ → suc ⁡ ⋃ A ∈ On
44 onsucuni ⊢ A ⊆ On → A ⊆ suc ⁡ ⋃ A
45 16 44 syl ⊢ φ → A ⊆ suc ⁡ ⋃ A
46 sseq2 ⊢ z = suc ⁡ ⋃ A → A ⊆ z ↔ A ⊆ suc ⁡ ⋃ A
47 46 rspcev ⊢ suc ⁡ ⋃ A ∈ On ∧ A ⊆ suc ⁡ ⋃ A → ∃ z ∈ On A ⊆ z
48 43 45 47 syl2anc ⊢ φ → ∃ z ∈ On A ⊆ z
49 onintrab2 ⊢ ∃ z ∈ On A ⊆ z ↔ ⋂ z ∈ On | A ⊆ z ∈ On
50 48 49 sylib ⊢ φ → ⋂ z ∈ On | A ⊆ z ∈ On
51 33 50 3 elrabd ⊢ φ → ⋂ z ∈ On | A ⊆ z ∈ w ∈ On | B ⊆ w
52 intss1 ⊢ ⋂ z ∈ On | A ⊆ z ∈ w ∈ On | B ⊆ w → ⋂ w ∈ On | B ⊆ w ⊆ ⋂ z ∈ On | A ⊆ z
53 51 52 syl ⊢ φ → ⋂ w ∈ On | B ⊆ w ⊆ ⋂ z ∈ On | A ⊆ z
54 32 53 eqssd ⊢ φ → ⋂ z ∈ On | A ⊆ z = ⋂ w ∈ On | B ⊆ w