Step | Hyp | Ref
| Expression |
1 | | alephfnon 9558 |
. . . . . . 7
⊢ ℵ
Fn On |
2 | | fnfun 6432 |
. . . . . . 7
⊢ (ℵ
Fn On → Fun ℵ) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ Fun
ℵ |
4 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ V) |
5 | | resfunexg 6982 |
. . . . . 6
⊢ ((Fun
ℵ ∧ 𝐴 ∈ V)
→ (ℵ ↾ 𝐴)
∈ V) |
6 | 3, 4, 5 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴) ∈ V) |
7 | | limelon 6229 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On) |
8 | | onss 7518 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ⊆ On) |
10 | | fnssres 6453 |
. . . . . . 7
⊢ ((ℵ
Fn On ∧ 𝐴 ⊆ On)
→ (ℵ ↾ 𝐴)
Fn 𝐴) |
11 | 1, 9, 10 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴) Fn 𝐴) |
12 | | fvres 6687 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((ℵ ↾ 𝐴)‘𝑦) = (ℵ‘𝑦)) |
13 | 12 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) = (ℵ‘𝑦)) |
14 | | alephord2i 9570 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
15 | 14 | imp 410 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴)) |
16 | 13, 15 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
17 | 7, 16 | sylan 583 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑦 ∈ 𝐴) → ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
18 | 17 | ralrimiva 3096 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∀𝑦 ∈ 𝐴 ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) |
19 | | fnfvrnss 6888 |
. . . . . . 7
⊢
(((ℵ ↾ 𝐴) Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 ((ℵ ↾ 𝐴)‘𝑦) ∈ (ℵ‘𝐴)) → ran (ℵ ↾ 𝐴) ⊆ (ℵ‘𝐴)) |
20 | 11, 18, 19 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ran (ℵ ↾
𝐴) ⊆
(ℵ‘𝐴)) |
21 | | df-f 6337 |
. . . . . 6
⊢ ((ℵ
↾ 𝐴):𝐴⟶(ℵ‘𝐴) ↔ ((ℵ ↾ 𝐴) Fn 𝐴 ∧ ran (ℵ ↾ 𝐴) ⊆ (ℵ‘𝐴))) |
22 | 11, 20, 21 | sylanbrc 586 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴)) |
23 | | alephsmo 9595 |
. . . . . 6
⊢ Smo
ℵ |
24 | 1 | fndmi 6435 |
. . . . . . 7
⊢ dom
ℵ = On |
25 | 7, 24 | eleqtrrdi 2844 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ dom ℵ) |
26 | | smores 8011 |
. . . . . 6
⊢ ((Smo
ℵ ∧ 𝐴 ∈ dom
ℵ) → Smo (ℵ ↾ 𝐴)) |
27 | 23, 25, 26 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → Smo (ℵ ↾
𝐴)) |
28 | | alephlim 9560 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦)) |
29 | 28 | eleq2d 2818 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (𝑥 ∈ (ℵ‘𝐴) ↔ 𝑥 ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦))) |
30 | | eliun 4882 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ∈ (ℵ‘𝑦)) |
31 | | alephon 9562 |
. . . . . . . . . 10
⊢
(ℵ‘𝑦)
∈ On |
32 | 31 | onelssi 6275 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℵ‘𝑦) → 𝑥 ⊆ (ℵ‘𝑦)) |
33 | 32 | reximi 3156 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐴 𝑥 ∈ (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
34 | 30, 33 | sylbi 220 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
35 | 29, 34 | syl6bi 256 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (𝑥 ∈ (ℵ‘𝐴) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
36 | 35 | ralrimiv 3095 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) |
37 | | feq1 6479 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (𝑓:𝐴⟶(ℵ‘𝐴) ↔ (ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴))) |
38 | | smoeq 8009 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (Smo 𝑓 ↔ Smo (ℵ ↾ 𝐴))) |
39 | | fveq1 6667 |
. . . . . . . . . . . 12
⊢ (𝑓 = (ℵ ↾ 𝐴) → (𝑓‘𝑦) = ((ℵ ↾ 𝐴)‘𝑦)) |
40 | 39, 12 | sylan9eq 2793 |
. . . . . . . . . . 11
⊢ ((𝑓 = (ℵ ↾ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑓‘𝑦) = (ℵ‘𝑦)) |
41 | 40 | sseq2d 3907 |
. . . . . . . . . 10
⊢ ((𝑓 = (ℵ ↾ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥 ⊆ (𝑓‘𝑦) ↔ 𝑥 ⊆ (ℵ‘𝑦))) |
42 | 41 | rexbidva 3205 |
. . . . . . . . 9
⊢ (𝑓 = (ℵ ↾ 𝐴) → (∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
43 | 42 | ralbidv 3109 |
. . . . . . . 8
⊢ (𝑓 = (ℵ ↾ 𝐴) → (∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦) ↔ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) |
44 | 37, 38, 43 | 3anbi123d 1437 |
. . . . . . 7
⊢ (𝑓 = (ℵ ↾ 𝐴) → ((𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) ↔ ((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾ 𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)))) |
45 | 44 | spcegv 3499 |
. . . . . 6
⊢ ((ℵ
↾ 𝐴) ∈ V →
(((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾
𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦)) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)))) |
46 | 45 | imp 410 |
. . . . 5
⊢
(((ℵ ↾ 𝐴) ∈ V ∧ ((ℵ ↾ 𝐴):𝐴⟶(ℵ‘𝐴) ∧ Smo (ℵ ↾ 𝐴) ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (ℵ‘𝑦))) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦))) |
47 | 6, 22, 27, 36, 46 | syl13anc 1373 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦))) |
48 | | alephon 9562 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ On |
49 | | cfcof 9767 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ On ∧ 𝐴 ∈
On) → (∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
50 | 48, 7, 49 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (∃𝑓(𝑓:𝐴⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑥 ∈ (ℵ‘𝐴)∃𝑦 ∈ 𝐴 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
51 | 47, 50 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |
52 | 51 | expcom 417 |
. 2
⊢ (Lim
𝐴 → (𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴))) |
53 | | cf0 9744 |
. . 3
⊢
(cf‘∅) = ∅ |
54 | | fvprc 6660 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(ℵ‘𝐴) =
∅) |
55 | 54 | fveq2d 6672 |
. . 3
⊢ (¬
𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘∅)) |
56 | | fvprc 6660 |
. . 3
⊢ (¬
𝐴 ∈ V →
(cf‘𝐴) =
∅) |
57 | 53, 55, 56 | 3eqtr4a 2799 |
. 2
⊢ (¬
𝐴 ∈ V →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |
58 | 52, 57 | pm2.61d1 183 |
1
⊢ (Lim
𝐴 →
(cf‘(ℵ‘𝐴)) = (cf‘𝐴)) |