Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
(ℵ‘∅)) |
2 | 1 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = ∅ →
(card‘(ℵ‘𝑥)) =
(card‘(ℵ‘∅))) |
3 | 2, 1 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = ∅ →
((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔ (card‘(ℵ‘∅))
= (ℵ‘∅))) |
4 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦)) |
5 | 4 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝑦 → (card‘(ℵ‘𝑥)) =
(card‘(ℵ‘𝑦))) |
6 | 5, 4 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = 𝑦 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦))) |
7 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) |
8 | 7 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (card‘(ℵ‘𝑥)) =
(card‘(ℵ‘suc 𝑦))) |
9 | 8, 7 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔
(card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦))) |
10 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝐴 → (ℵ‘𝑥) = (ℵ‘𝐴)) |
11 | 10 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝐴 → (card‘(ℵ‘𝑥)) =
(card‘(ℵ‘𝐴))) |
12 | 11, 10 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = 𝐴 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴))) |
13 | | cardom 8695 |
. . . 4
⊢
(card‘ω) = ω |
14 | | aleph0 8772 |
. . . . 5
⊢
(ℵ‘∅) = ω |
15 | 14 | fveq2i 6106 |
. . . 4
⊢
(card‘(ℵ‘∅)) =
(card‘ω) |
16 | 13, 15, 14 | 3eqtr4i 2642 |
. . 3
⊢
(card‘(ℵ‘∅)) =
(ℵ‘∅) |
17 | | harcard 8687 |
. . . . 5
⊢
(card‘(har‘(ℵ‘𝑦))) = (har‘(ℵ‘𝑦)) |
18 | | alephsuc 8774 |
. . . . . 6
⊢ (𝑦 ∈ On →
(ℵ‘suc 𝑦) =
(har‘(ℵ‘𝑦))) |
19 | 18 | fveq2d 6107 |
. . . . 5
⊢ (𝑦 ∈ On →
(card‘(ℵ‘suc 𝑦)) =
(card‘(har‘(ℵ‘𝑦)))) |
20 | 17, 19, 18 | 3eqtr4a 2670 |
. . . 4
⊢ (𝑦 ∈ On →
(card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦)) |
21 | 20 | a1d 25 |
. . 3
⊢ (𝑦 ∈ On →
((card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦))) |
22 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
23 | | cardiun 8691 |
. . . . . . 7
⊢ (𝑥 ∈ V → (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪
𝑦 ∈ 𝑥 (ℵ‘𝑦))) |
24 | 22, 23 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪
𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
25 | 24 | adantl 481 |
. . . . 5
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪
𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
26 | | alephlim 8773 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
27 | 22, 26 | mpan 702 |
. . . . . . 7
⊢ (Lim
𝑥 →
(ℵ‘𝑥) =
∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
28 | 27 | adantr 480 |
. . . . . 6
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
29 | 28 | fveq2d 6107 |
. . . . 5
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) →
(card‘(ℵ‘𝑥)) = (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))) |
30 | 25, 29, 28 | 3eqtr4d 2654 |
. . . 4
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) →
(card‘(ℵ‘𝑥)) = (ℵ‘𝑥)) |
31 | 30 | ex 449 |
. . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) →
(card‘(ℵ‘𝑥)) = (ℵ‘𝑥))) |
32 | 3, 6, 9, 12, 16, 21, 31 | tfinds 6951 |
. 2
⊢ (𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
33 | | card0 8667 |
. . 3
⊢
(card‘∅) = ∅ |
34 | | alephfnon 8771 |
. . . . . . 7
⊢ ℵ
Fn On |
35 | | fndm 5904 |
. . . . . . 7
⊢ (ℵ
Fn On → dom ℵ = On) |
36 | 34, 35 | ax-mp 5 |
. . . . . 6
⊢ dom
ℵ = On |
37 | 36 | eleq2i 2680 |
. . . . 5
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
38 | | ndmfv 6128 |
. . . . 5
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
39 | 37, 38 | sylnbir 320 |
. . . 4
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) =
∅) |
40 | 39 | fveq2d 6107 |
. . 3
⊢ (¬
𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (card‘∅)) |
41 | 33, 40, 39 | 3eqtr4a 2670 |
. 2
⊢ (¬
𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
42 | 32, 41 | pm2.61i 175 |
1
⊢
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴) |