| Step | Hyp | Ref
| Expression |
| 1 | | alephcard 10110 |
. . . 4
⊢
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ On →
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
| 3 | | alephgeom 10122 |
. . . 4
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
| 4 | 3 | biimpi 216 |
. . 3
⊢ (𝐴 ∈ On → ω
⊆ (ℵ‘𝐴)) |
| 5 | | alephord2i 10117 |
. . . . 5
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
| 6 | | elirr 9637 |
. . . . . . 7
⊢ ¬
(ℵ‘𝑦) ∈
(ℵ‘𝑦) |
| 7 | | eleq2 2830 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
(ℵ‘𝑦) →
((ℵ‘𝑦) ∈
(ℵ‘𝐴) ↔
(ℵ‘𝑦) ∈
(ℵ‘𝑦))) |
| 8 | 6, 7 | mtbiri 327 |
. . . . . 6
⊢
((ℵ‘𝐴) =
(ℵ‘𝑦) →
¬ (ℵ‘𝑦)
∈ (ℵ‘𝐴)) |
| 9 | 8 | con2i 139 |
. . . . 5
⊢
((ℵ‘𝑦)
∈ (ℵ‘𝐴)
→ ¬ (ℵ‘𝐴) = (ℵ‘𝑦)) |
| 10 | 5, 9 | syl6 35 |
. . . 4
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → ¬ (ℵ‘𝐴) = (ℵ‘𝑦))) |
| 11 | 10 | ralrimiv 3145 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦)) |
| 12 | | fvex 6919 |
. . . 4
⊢
(ℵ‘𝐴)
∈ V |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → (card‘𝑥) =
(card‘(ℵ‘𝐴))) |
| 14 | | id 22 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → 𝑥 = (ℵ‘𝐴)) |
| 15 | 13, 14 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → ((card‘𝑥) = 𝑥 ↔ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴))) |
| 16 | | sseq2 4010 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆
(ℵ‘𝐴))) |
| 17 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = (ℵ‘𝐴) → (𝑥 = (ℵ‘𝑦) ↔ (ℵ‘𝐴) = (ℵ‘𝑦))) |
| 18 | 17 | notbid 318 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝐴) → (¬ 𝑥 = (ℵ‘𝑦) ↔ ¬
(ℵ‘𝐴) =
(ℵ‘𝑦))) |
| 19 | 18 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦) ↔ ∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦))) |
| 20 | 15, 16, 19 | 3anbi123d 1438 |
. . . 4
⊢ (𝑥 = (ℵ‘𝐴) → (((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦)) ↔ ((card‘(ℵ‘𝐴)) = (ℵ‘𝐴) ∧ ω ⊆
(ℵ‘𝐴) ∧
∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦)))) |
| 21 | 12, 20 | elab 3679 |
. . 3
⊢
((ℵ‘𝐴)
∈ {𝑥 ∣
((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ ((card‘(ℵ‘𝐴)) = (ℵ‘𝐴) ∧ ω ⊆
(ℵ‘𝐴) ∧
∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝐴) = (ℵ‘𝑦))) |
| 22 | 2, 4, 11, 21 | syl3anbrc 1344 |
. 2
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ∈
{𝑥 ∣
((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |
| 23 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ∈ (ℵ‘𝐴) ↔ (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
| 24 | | alephord2 10116 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ 𝐴 ↔ (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
| 25 | 24 | bicomd 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ On) →
((ℵ‘𝑦) ∈
(ℵ‘𝐴) ↔
𝑦 ∈ 𝐴)) |
| 26 | 23, 25 | sylan9bbr 510 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → (𝑧 ∈ (ℵ‘𝐴) ↔ 𝑦 ∈ 𝐴)) |
| 27 | 26 | biimpcd 249 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (ℵ‘𝐴) → (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → 𝑦 ∈ 𝐴)) |
| 28 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → 𝑧 = (ℵ‘𝑦)) |
| 29 | 27, 28 | jca2 513 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (ℵ‘𝐴) → (((𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ 𝑧 = (ℵ‘𝑦)) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))) |
| 30 | 29 | exp4c 432 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (ℵ‘𝐴) → (𝑦 ∈ On → (𝐴 ∈ On → (𝑧 = (ℵ‘𝑦) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))))) |
| 31 | 30 | com3r 87 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝑧 ∈ (ℵ‘𝐴) → (𝑦 ∈ On → (𝑧 = (ℵ‘𝑦) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))))) |
| 32 | 31 | imp4b 421 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → ((𝑦 ∈ On ∧ 𝑧 = (ℵ‘𝑦)) → (𝑦 ∈ 𝐴 ∧ 𝑧 = (ℵ‘𝑦)))) |
| 33 | 32 | reximdv2 3164 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → (∃𝑦 ∈ On 𝑧 = (ℵ‘𝑦) → ∃𝑦 ∈ 𝐴 𝑧 = (ℵ‘𝑦))) |
| 34 | | cardalephex 10130 |
. . . . . . . . 9
⊢ (ω
⊆ 𝑧 →
((card‘𝑧) = 𝑧 ↔ ∃𝑦 ∈ On 𝑧 = (ℵ‘𝑦))) |
| 35 | 34 | biimpac 478 |
. . . . . . . 8
⊢
(((card‘𝑧) =
𝑧 ∧ ω ⊆
𝑧) → ∃𝑦 ∈ On 𝑧 = (ℵ‘𝑦)) |
| 36 | 33, 35 | impel 505 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) ∧ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧)) → ∃𝑦 ∈ 𝐴 𝑧 = (ℵ‘𝑦)) |
| 37 | | dfrex2 3073 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐴 𝑧 = (ℵ‘𝑦) ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)) |
| 38 | 36, 37 | sylib 218 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) ∧ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧)) → ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)) |
| 39 | | nan 830 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → ¬
(((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) ↔ (((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) ∧ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧)) → ¬ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 40 | 38, 39 | mpbir 231 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑧 ∈ (ℵ‘𝐴)) → ¬
(((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 41 | 40 | ex 412 |
. . . 4
⊢ (𝐴 ∈ On → (𝑧 ∈ (ℵ‘𝐴) → ¬
(((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)))) |
| 42 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 43 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (card‘𝑥) = (card‘𝑧)) |
| 44 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
| 45 | 43, 44 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((card‘𝑥) = 𝑥 ↔ (card‘𝑧) = 𝑧)) |
| 46 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (ω ⊆ 𝑥 ↔ ω ⊆ 𝑧)) |
| 47 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 = (ℵ‘𝑦) ↔ 𝑧 = (ℵ‘𝑦))) |
| 48 | 47 | notbid 318 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (¬ 𝑥 = (ℵ‘𝑦) ↔ ¬ 𝑧 = (ℵ‘𝑦))) |
| 49 | 48 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦) ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 50 | 45, 46, 49 | 3anbi123d 1438 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦)) ↔ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)))) |
| 51 | 42, 50 | elab 3679 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ ((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 52 | | df-3an 1089 |
. . . . . 6
⊢
(((card‘𝑧) =
𝑧 ∧ ω ⊆
𝑧 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦)) ↔ (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 53 | 51, 52 | bitri 275 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 54 | 53 | notbii 320 |
. . . 4
⊢ (¬
𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ↔ ¬ (((card‘𝑧) = 𝑧 ∧ ω ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑧 = (ℵ‘𝑦))) |
| 55 | 41, 54 | imbitrrdi 252 |
. . 3
⊢ (𝐴 ∈ On → (𝑧 ∈ (ℵ‘𝐴) → ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))})) |
| 56 | 55 | ralrimiv 3145 |
. 2
⊢ (𝐴 ∈ On → ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |
| 57 | | cardon 9984 |
. . . . . 6
⊢
(card‘𝑥)
∈ On |
| 58 | | eleq1 2829 |
. . . . . 6
⊢
((card‘𝑥) =
𝑥 → ((card‘𝑥) ∈ On ↔ 𝑥 ∈ On)) |
| 59 | 57, 58 | mpbii 233 |
. . . . 5
⊢
((card‘𝑥) =
𝑥 → 𝑥 ∈ On) |
| 60 | 59 | 3ad2ant1 1134 |
. . . 4
⊢
(((card‘𝑥) =
𝑥 ∧ ω ⊆
𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦)) → 𝑥 ∈ On) |
| 61 | 60 | abssi 4070 |
. . 3
⊢ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ⊆ On |
| 62 | | oneqmini 6436 |
. . 3
⊢ ({𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ⊆ On → (((ℵ‘𝐴) ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) → (ℵ‘𝐴) = ∩ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))})) |
| 63 | 61, 62 | ax-mp 5 |
. 2
⊢
(((ℵ‘𝐴)
∈ {𝑥 ∣
((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) → (ℵ‘𝐴) = ∩ {𝑥 ∣ ((card‘𝑥) = 𝑥 ∧ ω ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |
| 64 | 22, 56, 63 | syl2anc 584 |
1
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) = ∩ {𝑥
∣ ((card‘𝑥) =
𝑥 ∧ ω ⊆
𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 = (ℵ‘𝑦))}) |