Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6722 |
. . . 4
⊢ (𝑥 = ∅ →
(card‘(ℵ‘𝑥)) =
(card‘(ℵ‘∅))) |
2 | | fveq2 6717 |
. . . 4
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
(ℵ‘∅)) |
3 | 1, 2 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = ∅ →
((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔ (card‘(ℵ‘∅))
= (ℵ‘∅))) |
4 | | 2fveq3 6722 |
. . . 4
⊢ (𝑥 = 𝑦 → (card‘(ℵ‘𝑥)) =
(card‘(ℵ‘𝑦))) |
5 | | fveq2 6717 |
. . . 4
⊢ (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦)) |
6 | 4, 5 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝑦 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦))) |
7 | | 2fveq3 6722 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (card‘(ℵ‘𝑥)) =
(card‘(ℵ‘suc 𝑦))) |
8 | | fveq2 6717 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) |
9 | 7, 8 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔
(card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦))) |
10 | | 2fveq3 6722 |
. . . 4
⊢ (𝑥 = 𝐴 → (card‘(ℵ‘𝑥)) =
(card‘(ℵ‘𝐴))) |
11 | | fveq2 6717 |
. . . 4
⊢ (𝑥 = 𝐴 → (ℵ‘𝑥) = (ℵ‘𝐴)) |
12 | 10, 11 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝐴 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴))) |
13 | | cardom 9602 |
. . . 4
⊢
(card‘ω) = ω |
14 | | aleph0 9680 |
. . . . 5
⊢
(ℵ‘∅) = ω |
15 | 14 | fveq2i 6720 |
. . . 4
⊢
(card‘(ℵ‘∅)) =
(card‘ω) |
16 | 13, 15, 14 | 3eqtr4i 2775 |
. . 3
⊢
(card‘(ℵ‘∅)) =
(ℵ‘∅) |
17 | | harcard 9594 |
. . . . 5
⊢
(card‘(har‘(ℵ‘𝑦))) = (har‘(ℵ‘𝑦)) |
18 | | alephsuc 9682 |
. . . . . 6
⊢ (𝑦 ∈ On →
(ℵ‘suc 𝑦) =
(har‘(ℵ‘𝑦))) |
19 | 18 | fveq2d 6721 |
. . . . 5
⊢ (𝑦 ∈ On →
(card‘(ℵ‘suc 𝑦)) =
(card‘(har‘(ℵ‘𝑦)))) |
20 | 17, 19, 18 | 3eqtr4a 2804 |
. . . 4
⊢ (𝑦 ∈ On →
(card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦)) |
21 | 20 | a1d 25 |
. . 3
⊢ (𝑦 ∈ On →
((card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦))) |
22 | | cardiun 9598 |
. . . . . . 7
⊢ (𝑥 ∈ V → (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪
𝑦 ∈ 𝑥 (ℵ‘𝑦))) |
23 | 22 | elv 3414 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪
𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
24 | 23 | adantl 485 |
. . . . 5
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪
𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
25 | | vex 3412 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
26 | | alephlim 9681 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
27 | 25, 26 | mpan 690 |
. . . . . . 7
⊢ (Lim
𝑥 →
(ℵ‘𝑥) =
∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
28 | 27 | adantr 484 |
. . . . . 6
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) |
29 | 28 | fveq2d 6721 |
. . . . 5
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) →
(card‘(ℵ‘𝑥)) = (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))) |
30 | 24, 29, 28 | 3eqtr4d 2787 |
. . . 4
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) →
(card‘(ℵ‘𝑥)) = (ℵ‘𝑥)) |
31 | 30 | ex 416 |
. . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) →
(card‘(ℵ‘𝑥)) = (ℵ‘𝑥))) |
32 | 3, 6, 9, 12, 16, 21, 31 | tfinds 7638 |
. 2
⊢ (𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
33 | | card0 9574 |
. . 3
⊢
(card‘∅) = ∅ |
34 | | alephfnon 9679 |
. . . . . . 7
⊢ ℵ
Fn On |
35 | 34 | fndmi 6482 |
. . . . . 6
⊢ dom
ℵ = On |
36 | 35 | eleq2i 2829 |
. . . . 5
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
37 | | ndmfv 6747 |
. . . . 5
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
38 | 36, 37 | sylnbir 334 |
. . . 4
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) =
∅) |
39 | 38 | fveq2d 6721 |
. . 3
⊢ (¬
𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (card‘∅)) |
40 | 33, 39, 38 | 3eqtr4a 2804 |
. 2
⊢ (¬
𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
41 | 32, 40 | pm2.61i 185 |
1
⊢
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴) |