Step | Hyp | Ref
| Expression |
1 | | alephcard 8893 |
. . . 4
⊢
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
3 | | alephgeom 8905 |
. . . 4
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
4 | 3 | biimpi 206 |
. . 3
⊢ (𝐴 ∈ On → ω
⊆ (ℵ‘𝐴)) |
5 | | alephord2i 8900 |
. . . . 5
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
6 | | elirr 8505 |
. . . . . . 7
⊢ ¬
(ℵ‘𝑦) ∈
(ℵ‘𝑦) |
7 | | eleq2 2690 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
(ℵ‘𝑦) →
((ℵ‘𝑦) ∈
(ℵ‘𝐴) ↔
(ℵ‘𝑦) ∈
(ℵ‘𝑦))) |
8 | 6, 7 | mtbiri 317 |
. . . . . 6
⊢
((ℵ‘𝐴) =
(ℵ‘𝑦) →
¬ (ℵ‘𝑦)
∈ (ℵ‘𝐴)) |
9 | 8 | con2i 134 |
. . . . 5
⊢
((ℵ‘𝑦)
∈ (ℵ‘𝐴)
→ ¬ (ℵ‘𝐴) = (ℵ‘𝑦)) |
10 | 5, 9 | syl6 35 |
. . . 4
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → ¬ (ℵ‘𝐴) = (ℵ‘𝑦))) |
11 | 10 | ralrimiv 2965 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦)) |
12 | | fvex 6201 |
. . . 4
⊢
(ℵ‘𝐴)
∈ V |
13 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → (card‘𝑥) =
(card‘(ℵ‘𝐴))) |
14 | | id 22 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → 𝑥 = (ℵ‘𝐴)) |
15 | 13, 14 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → ((card‘𝑥) = 𝑥 ↔ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴))) |
16 | | sseq2 3627 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆
(ℵ‘𝐴))) |
17 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑥 = (ℵ‘𝐴) → (𝑥 = (ℵ‘𝑦) ↔ (ℵ‘𝐴) = (ℵ‘𝑦))) |
18 | 17 | notbid 308 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → (¬ 𝑥 = (ℵ‘𝑦) ↔ ¬
(ℵ‘𝐴) =
(ℵ‘𝑦))) |
19 | 18 | ralbidv 2986 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦) ↔ ∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦))) |
20 | 15, 16, 19 | 3anbi123d 1399 |
. . . 4
⊢ (𝑥 = (ℵ‘𝐴) → (((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦)) ↔ ((card‘(ℵ‘𝐴)) = (ℵ‘𝐴) ∧ ω ⊆
(ℵ‘𝐴) ∧
∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦)))) |
21 | 12, 20 | elab 3350 |
. . 3
⊢
((ℵ‘𝐴)
∈ {𝑥 ∣
((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ ((card‘(ℵ‘𝐴)) = (ℵ‘𝐴) ∧ ω ⊆
(ℵ‘𝐴) ∧
∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦))) |
22 | 2, 4, 11, 21 | syl3anbrc 1246 |
. 2
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ∈
{𝑥 ∣
((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |
23 | | cardalephex 8913 |
. . . . . . . . . 10
⊢ (ω
⊆ 𝑧 →
((card‘𝑧) = 𝑧 ↔ ∃𝑦 ∈ On 𝑧 = (ℵ‘𝑦))) |
24 | 23 | biimpac 503 |
. . . . . . . . 9
⊢
(((card‘𝑧) =
𝑧 ∧ ω ⊆
𝑧) → ∃𝑦 ∈ On 𝑧 = (ℵ‘𝑦)) |
25 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ∈ (ℵ‘𝐴) ↔ (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
26 | | alephord2 8899 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ 𝐴 ↔ (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
27 | 26 | bicomd 213 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On) →
((ℵ‘𝑦) ∈
(ℵ‘𝐴) ↔
𝑦 ∈ 𝐴)) |
28 | 25, 27 | sylan9bbr 737 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → (𝑧 ∈ (ℵ‘𝐴) ↔ 𝑦 ∈ 𝐴)) |
29 | 28 | biimpcd 239 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (ℵ‘𝐴) → (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → 𝑦 ∈ 𝐴)) |
30 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → 𝑧 = (ℵ‘𝑦)) |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (ℵ‘𝐴) → (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → 𝑧 = (ℵ‘𝑦))) |
32 | 29, 31 | jcad 555 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (ℵ‘𝐴) → (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))) |
33 | 32 | exp4c 636 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (ℵ‘𝐴) → (𝑦 ∈ On → (𝐴 ∈ On → (𝑧 = (ℵ‘𝑦) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))))) |
34 | 33 | com3r 87 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (𝑧 ∈ (ℵ‘𝐴) → (𝑦 ∈ On → (𝑧 = (ℵ‘𝑦) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))))) |
35 | 34 | imp4b 613 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → ((𝑦 ∈ On ∧ 𝑧 = (ℵ‘𝑦)) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))) |
36 | 35 | reximdv2 3014 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → (∃𝑦 ∈ On 𝑧 = (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑧 = (ℵ‘𝑦))) |
37 | 24, 36 | syl5 34 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) → ∃𝑦 ∈ 𝐴 𝑧 = (ℵ‘𝑦))) |
38 | 37 | imp 445 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) ∧ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧)) → ∃𝑦 ∈ 𝐴 𝑧 = (ℵ‘𝑦)) |
39 | | dfrex2 2996 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐴 𝑧 = (ℵ‘𝑦) ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)) |
40 | 38, 39 | sylib 208 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) ∧ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧)) → ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)) |
41 | | nan 604 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → ¬
(((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) ↔ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) ∧ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧)) → ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
42 | 40, 41 | mpbir 221 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → ¬
(((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
43 | 42 | ex 450 |
. . . 4
⊢ (𝐴 ∈ On → (𝑧 ∈ (ℵ‘𝐴) → ¬
(((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)))) |
44 | | vex 3203 |
. . . . . . 7
⊢ 𝑧 ∈ V |
45 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (card‘𝑥) = (card‘𝑧)) |
46 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
47 | 45, 46 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((card‘𝑥) = 𝑥 ↔ (card‘𝑧) = 𝑧)) |
48 | | sseq2 3627 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (ω ⊆ 𝑥 ↔ ω ⊆ 𝑧)) |
49 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 = (ℵ‘𝑦) ↔ 𝑧 = (ℵ‘𝑦))) |
50 | 49 | notbid 308 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (¬ 𝑥 = (ℵ‘𝑦) ↔ ¬ 𝑧 = (ℵ‘𝑦))) |
51 | 50 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦) ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
52 | 47, 48, 51 | 3anbi123d 1399 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦)) ↔ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)))) |
53 | 44, 52 | elab 3350 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
54 | | df-3an 1039 |
. . . . . 6
⊢
(((card‘𝑧) =
𝑧 ∧ ω ⊆
𝑧 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)) ↔ (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
55 | 53, 54 | bitri 264 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
56 | 55 | notbii 310 |
. . . 4
⊢ (¬
𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ ¬ (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
57 | 43, 56 | syl6ibr 242 |
. . 3
⊢ (𝐴 ∈ On → (𝑧 ∈ (ℵ‘𝐴) → ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))})) |
58 | 57 | ralrimiv 2965 |
. 2
⊢ (𝐴 ∈ On → ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |
59 | | cardon 8770 |
. . . . . 6
⊢
(card‘𝑥)
∈ On |
60 | | eleq1 2689 |
. . . . . 6
⊢
((card‘𝑥) =
𝑥 → ((card‘𝑥) ∈ On ↔ 𝑥 ∈ On)) |
61 | 59, 60 | mpbii 223 |
. . . . 5
⊢
((card‘𝑥) =
𝑥 → 𝑥 ∈ On) |
62 | 61 | 3ad2ant1 1082 |
. . . 4
⊢
(((card‘𝑥) =
𝑥 ∧ ω ⊆
𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦)) → 𝑥 ∈ On) |
63 | 62 | abssi 3677 |
. . 3
⊢ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ⊆ On |
64 | | oneqmini 5776 |
. . 3
⊢ ({𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ⊆ On → (((ℵ‘𝐴) ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) → (ℵ‘𝐴) = ∩ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))})) |
65 | 63, 64 | ax-mp 5 |
. 2
⊢
(((ℵ‘𝐴)
∈ {𝑥 ∣
((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) → (ℵ‘𝐴) = ∩ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |
66 | 22, 58, 65 | syl2anc 693 |
1
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) = ∩ {𝑥
∣ ((card‘𝑥) =
𝑥 ∧ ω ⊆
𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |