| Step | Hyp | Ref
| Expression |
| 1 | | alephfnon 10105 |
. . . . . . 7
⊢ ℵ
Fn On |
| 2 | | fnfun 6668 |
. . . . . . 7
⊢ (ℵ
Fn On → Fun ℵ) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ Fun
ℵ |
| 4 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ V) |
| 5 | | resfunexg 7235 |
. . . . . 6
⊢ ((Fun
ℵ ∧ 𝐴 ∈ V)
→ (ℵ ↾ 𝐴)
∈ V) |
| 6 | 3, 4, 5 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴) ∈ V) |
| 7 | | limelon 6448 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On) |
| 8 | | onss 7805 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ⊆ On) |
| 10 | | fnssres 6691 |
. . . . . . 7
⊢ ((ℵ
Fn On ∧ 𝐴 ⊆ On)
→ (ℵ ↾ 𝐴)
Fn 𝐴) |
| 11 | 1, 9, 10 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴) Fn 𝐴) |
| 12 | | fvres 6925 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((ℵ ↾ 𝐴)‘𝑦) = (ℵ‘𝑦)) |
| 13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) = (ℵ‘𝑦)) |
| 14 | | alephord2i 10117 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
| 15 | 14 | imp 406 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴)) |
| 16 | 13, 15 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
| 17 | 7, 16 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
| 18 | 17 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∀𝑦 ∈ 𝐴 ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
| 19 | | fnfvrnss 7141 |
. . . . . . 7
⊢
(((ℵ ↾ 𝐴) Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) → ran (ℵ ↾ 𝐴) ⊆ (ℵ‘𝐴)) |
| 20 | 11, 18, 19 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ran (ℵ ↾
𝐴) ⊆
(ℵ‘𝐴)) |
| 21 | | df-f 6565 |
. . . . . 6
⊢ ((ℵ
↾ 𝐴):𝐴⟶(ℵ‘𝐴) ↔ ((ℵ ↾ 𝐴) Fn 𝐴 ∧ ran (ℵ ↾ 𝐴) ⊆ (ℵ‘𝐴))) |
| 22 | 11, 20, 21 | sylanbrc 583 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴)) |
| 23 | | alephsmo 10142 |
. . . . . 6
⊢ Smo
ℵ |
| 24 | 1 | fndmi 6672 |
. . . . . . 7
⊢ dom
ℵ = On |
| 25 | 7, 24 | eleqtrrdi 2852 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ dom ℵ) |
| 26 | | smores 8392 |
. . . . . 6
⊢ ((Smo
ℵ ∧ 𝐴 ∈ dom
ℵ) → Smo (ℵ ↾ 𝐴)) |
| 27 | 23, 25, 26 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → Smo (ℵ ↾
𝐴)) |
| 28 | | alephlim 10107 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦)) |
| 29 | 28 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (𝑥 ∈ (ℵ‘𝐴) ↔ 𝑥 ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦))) |
| 30 | | eliun 4995 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ (ℵ‘𝑦)) |
| 31 | | alephon 10109 |
. . . . . . . . . 10
⊢
(ℵ‘𝑦)
∈ On |
| 32 | 31 | onelssi 6499 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℵ‘𝑦) → 𝑥 ⊆ (ℵ‘𝑦)) |
| 33 | 32 | reximi 3084 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐴 𝑥 ∈ (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
| 34 | 30, 33 | sylbi 217 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
| 35 | 29, 34 | biimtrdi 253 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (𝑥 ∈ (ℵ‘𝐴) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
| 36 | 35 | ralrimiv 3145 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
| 37 | | feq1 6716 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (𝑓:𝐴⟶(ℵ‘𝐴) ↔ (ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴))) |
| 38 | | smoeq 8390 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (Smo 𝑓 ↔ Smo (ℵ ↾ 𝐴))) |
| 39 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑓 = (ℵ ↾ 𝐴) → (𝑓‘𝑦) = ((ℵ ↾ 𝐴)‘𝑦)) |
| 40 | 39, 12 | sylan9eq 2797 |
. . . . . . . . . . 11
⊢ ((𝑓 = (ℵ ↾ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) = (ℵ‘𝑦)) |
| 41 | 40 | sseq2d 4016 |
. . . . . . . . . 10
⊢ ((𝑓 = (ℵ ↾ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ⊆ (ℵ‘𝑦))) |
| 42 | 41 | rexbidva 3177 |
. . . . . . . . 9
⊢ (𝑓 = (ℵ ↾ 𝐴) → (∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
| 43 | 42 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦) ↔ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
| 44 | 37, 38, 43 | 3anbi123d 1438 |
. . . . . . 7
⊢ (𝑓 = (ℵ ↾ 𝐴) → ((𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) ↔ ((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾ 𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)))) |
| 45 | 44 | spcegv 3597 |
. . . . . 6
⊢ ((ℵ
↾ 𝐴) ∈ V →
(((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾
𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)))) |
| 46 | 45 | imp 406 |
. . . . 5
⊢
(((ℵ ↾ 𝐴) ∈ V ∧ ((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾ 𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦))) |
| 47 | 6, 22, 27, 36, 46 | syl13anc 1374 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦))) |
| 48 | | alephon 10109 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ On |
| 49 | | cfcof 10314 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ On ∧ 𝐴 ∈
On) → (∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
| 50 | 48, 7, 49 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
| 51 | 47, 50 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |
| 52 | 51 | expcom 413 |
. 2
⊢ (Lim
𝐴 → (𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
| 53 | | cf0 10291 |
. . 3
⊢
(cf‘∅) = ∅ |
| 54 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(ℵ‘𝐴) =
∅) |
| 55 | 54 | fveq2d 6910 |
. . 3
⊢ (¬
𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘∅)) |
| 56 | | fvprc 6898 |
. . 3
⊢ (¬
𝐴 ∈ V →
(cf‘𝐴) =
∅) |
| 57 | 53, 55, 56 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |
| 58 | 52, 57 | pm2.61d1 180 |
1
⊢ (Lim
𝐴 →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |