Step | Hyp | Ref
| Expression |
1 | | alephfnon 9202 |
. . . . . . 7
⊢ ℵ
Fn On |
2 | | fnfun 6222 |
. . . . . . 7
⊢ (ℵ
Fn On → Fun ℵ) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ Fun
ℵ |
4 | | simpl 476 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ V) |
5 | | resfunexg 6736 |
. . . . . 6
⊢ ((Fun
ℵ ∧ 𝐴 ∈ V)
→ (ℵ ↾ 𝐴)
∈ V) |
6 | 3, 4, 5 | sylancr 583 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴) ∈ V) |
7 | | limelon 6027 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On) |
8 | | onss 7252 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ⊆ On) |
10 | | fnssres 6238 |
. . . . . . 7
⊢ ((ℵ
Fn On ∧ 𝐴 ⊆ On)
→ (ℵ ↾ 𝐴)
Fn 𝐴) |
11 | 1, 9, 10 | sylancr 583 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴) Fn 𝐴) |
12 | | fvres 6453 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((ℵ ↾ 𝐴)‘𝑦) = (ℵ‘𝑦)) |
13 | 12 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) = (ℵ‘𝑦)) |
14 | | alephord2i 9214 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
15 | 14 | imp 397 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴)) |
16 | 13, 15 | eqeltrd 2907 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
17 | 7, 16 | sylan 577 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
18 | 17 | ralrimiva 3176 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∀𝑦 ∈ 𝐴 ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
19 | | fnfvrnss 6640 |
. . . . . . 7
⊢
(((ℵ ↾ 𝐴) Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) → ran (ℵ ↾ 𝐴) ⊆ (ℵ‘𝐴)) |
20 | 11, 18, 19 | syl2anc 581 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ran (ℵ ↾
𝐴) ⊆
(ℵ‘𝐴)) |
21 | | df-f 6128 |
. . . . . 6
⊢ ((ℵ
↾ 𝐴):𝐴⟶(ℵ‘𝐴) ↔ ((ℵ ↾ 𝐴) Fn 𝐴 ∧ ran (ℵ ↾ 𝐴) ⊆ (ℵ‘𝐴))) |
22 | 11, 20, 21 | sylanbrc 580 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴)) |
23 | | alephsmo 9239 |
. . . . . 6
⊢ Smo
ℵ |
24 | | fndm 6224 |
. . . . . . . 8
⊢ (ℵ
Fn On → dom ℵ = On) |
25 | 1, 24 | ax-mp 5 |
. . . . . . 7
⊢ dom
ℵ = On |
26 | 7, 25 | syl6eleqr 2918 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ dom ℵ) |
27 | | smores 7716 |
. . . . . 6
⊢ ((Smo
ℵ ∧ 𝐴 ∈ dom
ℵ) → Smo (ℵ ↾ 𝐴)) |
28 | 23, 26, 27 | sylancr 583 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → Smo (ℵ ↾
𝐴)) |
29 | | alephlim 9204 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦)) |
30 | 29 | eleq2d 2893 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (𝑥 ∈ (ℵ‘𝐴) ↔ 𝑥 ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦))) |
31 | | eliun 4745 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ (ℵ‘𝑦)) |
32 | | alephon 9206 |
. . . . . . . . . 10
⊢
(ℵ‘𝑦)
∈ On |
33 | 32 | onelssi 6072 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℵ‘𝑦) → 𝑥 ⊆ (ℵ‘𝑦)) |
34 | 33 | reximi 3220 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐴 𝑥 ∈ (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
35 | 31, 34 | sylbi 209 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
36 | 30, 35 | syl6bi 245 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (𝑥 ∈ (ℵ‘𝐴) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
37 | 36 | ralrimiv 3175 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
38 | | feq1 6260 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (𝑓:𝐴⟶(ℵ‘𝐴) ↔ (ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴))) |
39 | | smoeq 7714 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (Smo 𝑓 ↔ Smo (ℵ ↾ 𝐴))) |
40 | | fveq1 6433 |
. . . . . . . . . . . 12
⊢ (𝑓 = (ℵ ↾ 𝐴) → (𝑓‘𝑦) = ((ℵ ↾ 𝐴)‘𝑦)) |
41 | 40, 12 | sylan9eq 2882 |
. . . . . . . . . . 11
⊢ ((𝑓 = (ℵ ↾ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) = (ℵ‘𝑦)) |
42 | 41 | sseq2d 3859 |
. . . . . . . . . 10
⊢ ((𝑓 = (ℵ ↾ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ⊆ (ℵ‘𝑦))) |
43 | 42 | rexbidva 3260 |
. . . . . . . . 9
⊢ (𝑓 = (ℵ ↾ 𝐴) → (∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
44 | 43 | ralbidv 3196 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦) ↔ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
45 | 38, 39, 44 | 3anbi123d 1566 |
. . . . . . 7
⊢ (𝑓 = (ℵ ↾ 𝐴) → ((𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) ↔ ((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾ 𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)))) |
46 | 45 | spcegv 3512 |
. . . . . 6
⊢ ((ℵ
↾ 𝐴) ∈ V →
(((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾
𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)))) |
47 | 46 | imp 397 |
. . . . 5
⊢
(((ℵ ↾ 𝐴) ∈ V ∧ ((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾ 𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦))) |
48 | 6, 22, 28, 37, 47 | syl13anc 1497 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦))) |
49 | | alephon 9206 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ On |
50 | | cfcof 9412 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ On ∧ 𝐴 ∈
On) → (∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
51 | 49, 7, 50 | sylancr 583 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
52 | 48, 51 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |
53 | 52 | expcom 404 |
. 2
⊢ (Lim
𝐴 → (𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
54 | | cf0 9389 |
. . 3
⊢
(cf‘∅) = ∅ |
55 | | fvprc 6427 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(ℵ‘𝐴) =
∅) |
56 | 55 | fveq2d 6438 |
. . 3
⊢ (¬
𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘∅)) |
57 | | fvprc 6427 |
. . 3
⊢ (¬
𝐴 ∈ V →
(cf‘𝐴) =
∅) |
58 | 54, 56, 57 | 3eqtr4a 2888 |
. 2
⊢ (¬
𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |
59 | 53, 58 | pm2.61d1 173 |
1
⊢ (Lim
𝐴 →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |