Step | Hyp | Ref
| Expression |
1 | | alephordilem1 9830 |
. . . 4
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) |
2 | | alephon 9826 |
. . . . . . . . 9
⊢
(ℵ‘suc 𝐴) ∈ On |
3 | | cff1 10015 |
. . . . . . . . 9
⊢
((ℵ‘suc 𝐴) ∈ On → ∃𝑓(𝑓:(cf‘(ℵ‘suc 𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦))) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
⊢
∃𝑓(𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) |
5 | | fvex 6784 |
. . . . . . . . . . . . 13
⊢
(cf‘(ℵ‘suc 𝐴)) ∈ V |
6 | | fvex 6784 |
. . . . . . . . . . . . . 14
⊢ (𝑓‘𝑦) ∈ V |
7 | 6 | sucex 7650 |
. . . . . . . . . . . . 13
⊢ suc
(𝑓‘𝑦) ∈ V |
8 | 5, 7 | iunex 7804 |
. . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ∈ V |
9 | | f1f 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) → 𝑓:(cf‘(ℵ‘suc 𝐴))⟶(ℵ‘suc
𝐴)) |
10 | 9 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → 𝑓:(cf‘(ℵ‘suc 𝐴))⟶(ℵ‘suc
𝐴)) |
11 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) |
12 | 2 | oneli 6373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (ℵ‘suc 𝐴) → 𝑥 ∈ On) |
13 | | ffvelrn 6956 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))) → (𝑓‘𝑦) ∈ (ℵ‘suc 𝐴)) |
14 | | onelon 6290 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ℵ‘suc 𝐴) ∈ On ∧ (𝑓‘𝑦) ∈ (ℵ‘suc 𝐴)) → (𝑓‘𝑦) ∈ On) |
15 | 2, 13, 14 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))) → (𝑓‘𝑦) ∈ On) |
16 | | onsssuc 6352 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ On ∧ (𝑓‘𝑦) ∈ On) → (𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ∈ suc (𝑓‘𝑦))) |
17 | 15, 16 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ (𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴)))) → (𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ∈ suc (𝑓‘𝑦))) |
18 | 17 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴)) ∧ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))) → (𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ∈ suc (𝑓‘𝑦))) |
19 | 18 | rexbidva 3227 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ On ∧ 𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴)) → (∃𝑦 ∈
(cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ∈ suc (𝑓‘𝑦))) |
20 | | eliun 4934 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ↔ ∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ∈ suc (𝑓‘𝑦)) |
21 | 19, 20 | bitr4di 289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ 𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴)) → (∃𝑦 ∈
(cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ∈ ∪
𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦))) |
22 | 21 | ancoms 459 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ∈ ∪
𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦))) |
23 | 12, 22 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ 𝑥 ∈ (ℵ‘suc 𝐴)) → (∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ∈ ∪
𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦))) |
24 | 23 | ralbidva 3122 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) → (∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦) ↔ ∀𝑥 ∈ (ℵ‘suc 𝐴)𝑥 ∈ ∪
𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦))) |
25 | | dfss3 3914 |
. . . . . . . . . . . . . . 15
⊢
((ℵ‘suc 𝐴) ⊆ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ↔ ∀𝑥 ∈ (ℵ‘suc 𝐴)𝑥 ∈ ∪
𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦)) |
26 | 24, 25 | bitr4di 289 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) → (∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦) ↔ (ℵ‘suc 𝐴) ⊆ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦))) |
27 | 26 | biimpa 477 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) → (ℵ‘suc 𝐴) ⊆ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦)) |
28 | 10, 11, 27 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → (ℵ‘suc
𝐴) ⊆ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦)) |
29 | | ssdomg 8769 |
. . . . . . . . . . . 12
⊢ (∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ∈ V → ((ℵ‘suc 𝐴) ⊆ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) → (ℵ‘suc 𝐴) ≼ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦))) |
30 | 8, 28, 29 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → (ℵ‘suc
𝐴) ≼ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦)) |
31 | | simprl 768 |
. . . . . . . . . . . 12
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → 𝐴 ∈ On) |
32 | | suceloni 7653 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
33 | | alephislim 9840 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝐴 ∈ On ↔ Lim
(ℵ‘suc 𝐴)) |
34 | | limsuc 7690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
(ℵ‘suc 𝐴)
→ ((𝑓‘𝑦) ∈ (ℵ‘suc
𝐴) ↔ suc (𝑓‘𝑦) ∈ (ℵ‘suc 𝐴))) |
35 | 33, 34 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝐴 ∈ On → ((𝑓‘𝑦) ∈ (ℵ‘suc 𝐴) ↔ suc (𝑓‘𝑦) ∈ (ℵ‘suc 𝐴))) |
36 | 32, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → ((𝑓‘𝑦) ∈ (ℵ‘suc 𝐴) ↔ suc (𝑓‘𝑦) ∈ (ℵ‘suc 𝐴))) |
37 | | breq1 5082 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = suc (𝑓‘𝑦) → (𝑧 ≺ (ℵ‘suc 𝐴) ↔ suc (𝑓‘𝑦) ≺ (ℵ‘suc 𝐴))) |
38 | | alephcard 9827 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(card‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴) |
39 | | iscard 9734 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((card‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴) ↔ ((ℵ‘suc 𝐴) ∈ On ∧ ∀𝑧 ∈ (ℵ‘suc 𝐴)𝑧 ≺ (ℵ‘suc 𝐴))) |
40 | 39 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((card‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴) → ∀𝑧 ∈ (ℵ‘suc 𝐴)𝑧 ≺ (ℵ‘suc 𝐴)) |
41 | 38, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
∀𝑧 ∈
(ℵ‘suc 𝐴)𝑧 ≺ (ℵ‘suc
𝐴) |
42 | 37, 41 | vtoclri 3524 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
(𝑓‘𝑦) ∈ (ℵ‘suc 𝐴) → suc (𝑓‘𝑦) ≺ (ℵ‘suc 𝐴)) |
43 | | alephsucdom 9836 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ On → (suc (𝑓‘𝑦) ≼ (ℵ‘𝐴) ↔ suc (𝑓‘𝑦) ≺ (ℵ‘suc 𝐴))) |
44 | 42, 43 | syl5ibr 245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → (suc (𝑓‘𝑦) ∈ (ℵ‘suc 𝐴) → suc (𝑓‘𝑦) ≼ (ℵ‘𝐴))) |
45 | 36, 44 | sylbid 239 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On → ((𝑓‘𝑦) ∈ (ℵ‘suc 𝐴) → suc (𝑓‘𝑦) ≼ (ℵ‘𝐴))) |
46 | 13, 45 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → ((𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴) ∧ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))) → suc (𝑓‘𝑦) ≼ (ℵ‘𝐴))) |
47 | 46 | expdimp 453 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴)) → (𝑦 ∈ (cf‘(ℵ‘suc 𝐴)) → suc (𝑓‘𝑦) ≼ (ℵ‘𝐴))) |
48 | 47 | ralrimiv 3109 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴)) → ∀𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ≼ (ℵ‘𝐴)) |
49 | | iundom 10299 |
. . . . . . . . . . . . 13
⊢
(((cf‘(ℵ‘suc 𝐴)) ∈ V ∧ ∀𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ≼ (ℵ‘𝐴)) → ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ≼ ((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) |
50 | 5, 48, 49 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑓:(cf‘(ℵ‘suc
𝐴))⟶(ℵ‘suc 𝐴)) → ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ≼ ((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) |
51 | 31, 10, 50 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ≼ ((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) |
52 | | domtr 8776 |
. . . . . . . . . . 11
⊢
(((ℵ‘suc 𝐴) ≼ ∪ 𝑦 ∈ (cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ∧ ∪
𝑦 ∈
(cf‘(ℵ‘suc 𝐴))suc (𝑓‘𝑦) ≼ ((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) → (ℵ‘suc
𝐴) ≼
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) |
53 | 30, 51, 52 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑓:(cf‘(ℵ‘suc
𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) ∧ (𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴))) → (ℵ‘suc
𝐴) ≼
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) |
54 | 53 | expcom 414 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) → ((𝑓:(cf‘(ℵ‘suc 𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) → (ℵ‘suc 𝐴) ≼
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)))) |
55 | 54 | exlimdv 1940 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) → (∃𝑓(𝑓:(cf‘(ℵ‘suc 𝐴))–1-1→(ℵ‘suc 𝐴) ∧ ∀𝑥 ∈ (ℵ‘suc 𝐴)∃𝑦 ∈ (cf‘(ℵ‘suc 𝐴))𝑥 ⊆ (𝑓‘𝑦)) → (ℵ‘suc 𝐴) ≼
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)))) |
56 | 4, 55 | mpi 20 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) → (ℵ‘suc
𝐴) ≼
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴))) |
57 | | alephgeom 9839 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
58 | | alephon 9826 |
. . . . . . . . . . 11
⊢
(ℵ‘𝐴)
∈ On |
59 | | infxpen 9771 |
. . . . . . . . . . 11
⊢
(((ℵ‘𝐴)
∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) |
60 | 58, 59 | mpan 687 |
. . . . . . . . . 10
⊢ (ω
⊆ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
× (ℵ‘𝐴))
≈ (ℵ‘𝐴)) |
61 | 57, 60 | sylbi 216 |
. . . . . . . . 9
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ×
(ℵ‘𝐴)) ≈
(ℵ‘𝐴)) |
62 | | breq1 5082 |
. . . . . . . . . . . 12
⊢ (𝑧 = (cf‘(ℵ‘suc
𝐴)) → (𝑧 ≺ (ℵ‘suc
𝐴) ↔
(cf‘(ℵ‘suc 𝐴)) ≺ (ℵ‘suc 𝐴))) |
63 | 62, 41 | vtoclri 3524 |
. . . . . . . . . . 11
⊢
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) →
(cf‘(ℵ‘suc 𝐴)) ≺ (ℵ‘suc 𝐴)) |
64 | | alephsucdom 9836 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘suc 𝐴)) ≼ (ℵ‘𝐴) ↔ (cf‘(ℵ‘suc 𝐴)) ≺ (ℵ‘suc
𝐴))) |
65 | 63, 64 | syl5ibr 245 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) →
(cf‘(ℵ‘suc 𝐴)) ≼ (ℵ‘𝐴))) |
66 | | fvex 6784 |
. . . . . . . . . . 11
⊢
(ℵ‘𝐴)
∈ V |
67 | 66 | xpdom1 8840 |
. . . . . . . . . 10
⊢
((cf‘(ℵ‘suc 𝐴)) ≼ (ℵ‘𝐴) → ((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴))) |
68 | 65, 67 | syl6 35 |
. . . . . . . . 9
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) →
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)))) |
69 | | domentr 8782 |
. . . . . . . . . 10
⊢
((((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)) ∧ ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) → ((cf‘(ℵ‘suc
𝐴)) ×
(ℵ‘𝐴)) ≼
(ℵ‘𝐴)) |
70 | 69 | expcom 414 |
. . . . . . . . 9
⊢
(((ℵ‘𝐴)
× (ℵ‘𝐴))
≈ (ℵ‘𝐴)
→ (((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴)) → ((cf‘(ℵ‘suc
𝐴)) ×
(ℵ‘𝐴)) ≼
(ℵ‘𝐴))) |
71 | 61, 68, 70 | sylsyld 61 |
. . . . . . . 8
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) →
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ (ℵ‘𝐴))) |
72 | 71 | imp 407 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) →
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ (ℵ‘𝐴)) |
73 | | domtr 8776 |
. . . . . . 7
⊢
(((ℵ‘suc 𝐴) ≼ ((cf‘(ℵ‘suc
𝐴)) ×
(ℵ‘𝐴)) ∧
((cf‘(ℵ‘suc 𝐴)) × (ℵ‘𝐴)) ≼ (ℵ‘𝐴)) → (ℵ‘suc 𝐴) ≼ (ℵ‘𝐴)) |
74 | 56, 72, 73 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) → (ℵ‘suc
𝐴) ≼
(ℵ‘𝐴)) |
75 | | domnsym 8868 |
. . . . . 6
⊢
((ℵ‘suc 𝐴) ≼ (ℵ‘𝐴) → ¬ (ℵ‘𝐴) ≺ (ℵ‘suc
𝐴)) |
76 | 74, 75 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) → ¬
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) |
77 | 76 | ex 413 |
. . . 4
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) → ¬
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴))) |
78 | 1, 77 | mt2d 136 |
. . 3
⊢ (𝐴 ∈ On → ¬
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴)) |
79 | | cfon 10012 |
. . . . 5
⊢
(cf‘(ℵ‘suc 𝐴)) ∈ On |
80 | | cfle 10011 |
. . . . . 6
⊢
(cf‘(ℵ‘suc 𝐴)) ⊆ (ℵ‘suc 𝐴) |
81 | | onsseleq 6306 |
. . . . . 6
⊢
(((cf‘(ℵ‘suc 𝐴)) ∈ On ∧ (ℵ‘suc 𝐴) ∈ On) →
((cf‘(ℵ‘suc 𝐴)) ⊆ (ℵ‘suc 𝐴) ↔
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) ∨
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴)))) |
82 | 80, 81 | mpbii 232 |
. . . . 5
⊢
(((cf‘(ℵ‘suc 𝐴)) ∈ On ∧ (ℵ‘suc 𝐴) ∈ On) →
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) ∨
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴))) |
83 | 79, 2, 82 | mp2an 689 |
. . . 4
⊢
((cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) ∨
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴)) |
84 | 83 | ori 858 |
. . 3
⊢ (¬
(cf‘(ℵ‘suc 𝐴)) ∈ (ℵ‘suc 𝐴) →
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴)) |
85 | 78, 84 | syl 17 |
. 2
⊢ (𝐴 ∈ On →
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴)) |
86 | | cf0 10008 |
. . 3
⊢
(cf‘∅) = ∅ |
87 | | alephfnon 9822 |
. . . . . . . 8
⊢ ℵ
Fn On |
88 | 87 | fndmi 6535 |
. . . . . . 7
⊢ dom
ℵ = On |
89 | 88 | eleq2i 2832 |
. . . . . 6
⊢ (suc
𝐴 ∈ dom ℵ ↔
suc 𝐴 ∈
On) |
90 | | sucelon 7658 |
. . . . . 6
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) |
91 | 89, 90 | bitr4i 277 |
. . . . 5
⊢ (suc
𝐴 ∈ dom ℵ ↔
𝐴 ∈
On) |
92 | | ndmfv 6801 |
. . . . 5
⊢ (¬
suc 𝐴 ∈ dom ℵ
→ (ℵ‘suc 𝐴) = ∅) |
93 | 91, 92 | sylnbir 331 |
. . . 4
⊢ (¬
𝐴 ∈ On →
(ℵ‘suc 𝐴) =
∅) |
94 | 93 | fveq2d 6775 |
. . 3
⊢ (¬
𝐴 ∈ On →
(cf‘(ℵ‘suc 𝐴)) = (cf‘∅)) |
95 | 86, 94, 93 | 3eqtr4a 2806 |
. 2
⊢ (¬
𝐴 ∈ On →
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴)) |
96 | 85, 95 | pm2.61i 182 |
1
⊢
(cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴) |