Step | Hyp | Ref
| Expression |
1 | | alephon 9483 |
. . . . . . . 8
⊢
(ℵ‘𝐴)
∈ On |
2 | | id 22 |
. . . . . . . . . 10
⊢
((card‘𝐵) =
𝐵 → (card‘𝐵) = 𝐵) |
3 | | cardon 9361 |
. . . . . . . . . 10
⊢
(card‘𝐵)
∈ On |
4 | 2, 3 | syl6eqelr 2919 |
. . . . . . . . 9
⊢
((card‘𝐵) =
𝐵 → 𝐵 ∈ On) |
5 | | onenon 9366 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → 𝐵 ∈ dom
card) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢
((card‘𝐵) =
𝐵 → 𝐵 ∈ dom card) |
7 | | cardsdomel 9391 |
. . . . . . . 8
⊢
(((ℵ‘𝐴)
∈ On ∧ 𝐵 ∈
dom card) → ((ℵ‘𝐴) ≺ 𝐵 ↔ (ℵ‘𝐴) ∈ (card‘𝐵))) |
8 | 1, 6, 7 | sylancr 587 |
. . . . . . 7
⊢
((card‘𝐵) =
𝐵 →
((ℵ‘𝐴) ≺
𝐵 ↔
(ℵ‘𝐴) ∈
(card‘𝐵))) |
9 | | eleq2 2898 |
. . . . . . 7
⊢
((card‘𝐵) =
𝐵 →
((ℵ‘𝐴) ∈
(card‘𝐵) ↔
(ℵ‘𝐴) ∈
𝐵)) |
10 | 8, 9 | bitrd 280 |
. . . . . 6
⊢
((card‘𝐵) =
𝐵 →
((ℵ‘𝐴) ≺
𝐵 ↔
(ℵ‘𝐴) ∈
𝐵)) |
11 | 10 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ((ℵ‘𝐴) ≺ 𝐵 ↔ (ℵ‘𝐴) ∈ 𝐵)) |
12 | | alephsuc 9482 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
(ℵ‘suc 𝐴) =
(har‘(ℵ‘𝐴))) |
13 | | onenon 9366 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝐴)
∈ On → (ℵ‘𝐴) ∈ dom card) |
14 | | harval2 9414 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝐴)
∈ dom card → (har‘(ℵ‘𝐴)) = ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥}) |
15 | 1, 13, 14 | mp2b 10 |
. . . . . . . . . . 11
⊢
(har‘(ℵ‘𝐴)) = ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥} |
16 | 12, 15 | syl6eq 2869 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
(ℵ‘suc 𝐴) =
∩ {𝑥 ∈ On ∣ (ℵ‘𝐴) ≺ 𝑥}) |
17 | 16 | eleq2d 2895 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐵 ∈ (ℵ‘suc 𝐴) ↔ 𝐵 ∈ ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥})) |
18 | 17 | biimpd 230 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐵 ∈ (ℵ‘suc 𝐴) → 𝐵 ∈ ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥})) |
19 | | breq2 5061 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((ℵ‘𝐴) ≺ 𝑥 ↔ (ℵ‘𝐴) ≺ 𝐵)) |
20 | 19 | onnminsb 7508 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐵 ∈ ∩ {𝑥
∈ On ∣ (ℵ‘𝐴) ≺ 𝑥} → ¬ (ℵ‘𝐴) ≺ 𝐵)) |
21 | 18, 20 | sylan9 508 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ∈ (ℵ‘suc 𝐴) → ¬
(ℵ‘𝐴) ≺
𝐵)) |
22 | 21 | con2d 136 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
((ℵ‘𝐴) ≺
𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴))) |
23 | 4, 22 | sylan2 592 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ((ℵ‘𝐴) ≺ 𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴))) |
24 | 11, 23 | sylbird 261 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ((ℵ‘𝐴) ∈ 𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴))) |
25 | | imnan 400 |
. . . 4
⊢
(((ℵ‘𝐴)
∈ 𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴)) ↔ ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |
26 | 24, 25 | sylib 219 |
. . 3
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |
27 | 26 | ex 413 |
. 2
⊢ (𝐴 ∈ On →
((card‘𝐵) = 𝐵 → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)))) |
28 | | n0i 4296 |
. . . . . . 7
⊢ (𝐵 ∈ (ℵ‘suc 𝐴) → ¬
(ℵ‘suc 𝐴) =
∅) |
29 | | alephfnon 9479 |
. . . . . . . . . 10
⊢ ℵ
Fn On |
30 | | fndm 6448 |
. . . . . . . . . 10
⊢ (ℵ
Fn On → dom ℵ = On) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
ℵ = On |
32 | 31 | eleq2i 2901 |
. . . . . . . 8
⊢ (suc
𝐴 ∈ dom ℵ ↔
suc 𝐴 ∈
On) |
33 | | ndmfv 6693 |
. . . . . . . 8
⊢ (¬
suc 𝐴 ∈ dom ℵ
→ (ℵ‘suc 𝐴) = ∅) |
34 | 32, 33 | sylnbir 332 |
. . . . . . 7
⊢ (¬
suc 𝐴 ∈ On →
(ℵ‘suc 𝐴) =
∅) |
35 | 28, 34 | nsyl2 143 |
. . . . . 6
⊢ (𝐵 ∈ (ℵ‘suc 𝐴) → suc 𝐴 ∈ On) |
36 | | sucelon 7521 |
. . . . . 6
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) |
37 | 35, 36 | sylibr 235 |
. . . . 5
⊢ (𝐵 ∈ (ℵ‘suc 𝐴) → 𝐴 ∈ On) |
38 | 37 | adantl 482 |
. . . 4
⊢
(((ℵ‘𝐴)
∈ 𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)) → 𝐴 ∈ On) |
39 | 38 | con3i 157 |
. . 3
⊢ (¬
𝐴 ∈ On → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |
40 | 39 | a1d 25 |
. 2
⊢ (¬
𝐴 ∈ On →
((card‘𝐵) = 𝐵 → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)))) |
41 | 27, 40 | pm2.61i 183 |
1
⊢
((card‘𝐵) =
𝐵 → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |