| Step | Hyp | Ref
| Expression |
| 1 | | alephon 10109 |
. . . . . . . 8
⊢
(ℵ‘𝐴)
∈ On |
| 2 | | id 22 |
. . . . . . . . . 10
⊢
((card‘𝐵) =
𝐵 → (card‘𝐵) = 𝐵) |
| 3 | | cardon 9984 |
. . . . . . . . . 10
⊢
(card‘𝐵)
∈ On |
| 4 | 2, 3 | eqeltrrdi 2850 |
. . . . . . . . 9
⊢
((card‘𝐵) =
𝐵 → 𝐵 ∈ On) |
| 5 | | onenon 9989 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → 𝐵 ∈ dom
card) |
| 6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢
((card‘𝐵) =
𝐵 → 𝐵 ∈ dom card) |
| 7 | | cardsdomel 10014 |
. . . . . . . 8
⊢
(((ℵ‘𝐴)
∈ On ∧ 𝐵 ∈
dom card) → ((ℵ‘𝐴) ≺ 𝐵 ↔ (ℵ‘𝐴) ∈ (card‘𝐵))) |
| 8 | 1, 6, 7 | sylancr 587 |
. . . . . . 7
⊢
((card‘𝐵) =
𝐵 →
((ℵ‘𝐴) ≺
𝐵 ↔
(ℵ‘𝐴) ∈
(card‘𝐵))) |
| 9 | | eleq2 2830 |
. . . . . . 7
⊢
((card‘𝐵) =
𝐵 →
((ℵ‘𝐴) ∈
(card‘𝐵) ↔
(ℵ‘𝐴) ∈
𝐵)) |
| 10 | 8, 9 | bitrd 279 |
. . . . . 6
⊢
((card‘𝐵) =
𝐵 →
((ℵ‘𝐴) ≺
𝐵 ↔
(ℵ‘𝐴) ∈
𝐵)) |
| 11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ((ℵ‘𝐴) ≺ 𝐵 ↔ (ℵ‘𝐴) ∈ 𝐵)) |
| 12 | | alephsuc 10108 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
(ℵ‘suc 𝐴) =
(har‘(ℵ‘𝐴))) |
| 13 | | onenon 9989 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝐴)
∈ On → (ℵ‘𝐴) ∈ dom card) |
| 14 | | harval2 10037 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝐴)
∈ dom card → (har‘(ℵ‘𝐴)) = ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥}) |
| 15 | 1, 13, 14 | mp2b 10 |
. . . . . . . . . . 11
⊢
(har‘(ℵ‘𝐴)) = ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥} |
| 16 | 12, 15 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
(ℵ‘suc 𝐴) =
∩ {𝑥 ∈ On ∣ (ℵ‘𝐴) ≺ 𝑥}) |
| 17 | 16 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐵 ∈ (ℵ‘suc 𝐴) ↔ 𝐵 ∈ ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥})) |
| 18 | 17 | biimpd 229 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐵 ∈ (ℵ‘suc 𝐴) → 𝐵 ∈ ∩ {𝑥 ∈ On ∣
(ℵ‘𝐴) ≺
𝑥})) |
| 19 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((ℵ‘𝐴) ≺ 𝑥 ↔ (ℵ‘𝐴) ≺ 𝐵)) |
| 20 | 19 | onnminsb 7819 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐵 ∈ ∩ {𝑥
∈ On ∣ (ℵ‘𝐴) ≺ 𝑥} → ¬ (ℵ‘𝐴) ≺ 𝐵)) |
| 21 | 18, 20 | sylan9 507 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ∈ (ℵ‘suc 𝐴) → ¬
(ℵ‘𝐴) ≺
𝐵)) |
| 22 | 21 | con2d 134 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
((ℵ‘𝐴) ≺
𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴))) |
| 23 | 4, 22 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ((ℵ‘𝐴) ≺ 𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴))) |
| 24 | 11, 23 | sylbird 260 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ((ℵ‘𝐴) ∈ 𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴))) |
| 25 | | imnan 399 |
. . . 4
⊢
(((ℵ‘𝐴)
∈ 𝐵 → ¬ 𝐵 ∈ (ℵ‘suc 𝐴)) ↔ ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |
| 26 | 24, 25 | sylib 218 |
. . 3
⊢ ((𝐴 ∈ On ∧
(card‘𝐵) = 𝐵) → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |
| 27 | 26 | ex 412 |
. 2
⊢ (𝐴 ∈ On →
((card‘𝐵) = 𝐵 → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)))) |
| 28 | | n0i 4340 |
. . . . . . 7
⊢ (𝐵 ∈ (ℵ‘suc 𝐴) → ¬
(ℵ‘suc 𝐴) =
∅) |
| 29 | | alephfnon 10105 |
. . . . . . . . . 10
⊢ ℵ
Fn On |
| 30 | 29 | fndmi 6672 |
. . . . . . . . 9
⊢ dom
ℵ = On |
| 31 | 30 | eleq2i 2833 |
. . . . . . . 8
⊢ (suc
𝐴 ∈ dom ℵ ↔
suc 𝐴 ∈
On) |
| 32 | | ndmfv 6941 |
. . . . . . . 8
⊢ (¬
suc 𝐴 ∈ dom ℵ
→ (ℵ‘suc 𝐴) = ∅) |
| 33 | 31, 32 | sylnbir 331 |
. . . . . . 7
⊢ (¬
suc 𝐴 ∈ On →
(ℵ‘suc 𝐴) =
∅) |
| 34 | 28, 33 | nsyl2 141 |
. . . . . 6
⊢ (𝐵 ∈ (ℵ‘suc 𝐴) → suc 𝐴 ∈ On) |
| 35 | | onsucb 7837 |
. . . . . 6
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) |
| 36 | 34, 35 | sylibr 234 |
. . . . 5
⊢ (𝐵 ∈ (ℵ‘suc 𝐴) → 𝐴 ∈ On) |
| 37 | 36 | adantl 481 |
. . . 4
⊢
(((ℵ‘𝐴)
∈ 𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)) → 𝐴 ∈ On) |
| 38 | 37 | con3i 154 |
. . 3
⊢ (¬
𝐴 ∈ On → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |
| 39 | 38 | a1d 25 |
. 2
⊢ (¬
𝐴 ∈ On →
((card‘𝐵) = 𝐵 → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)))) |
| 40 | 27, 39 | pm2.61i 182 |
1
⊢
((card‘𝐵) =
𝐵 → ¬
((ℵ‘𝐴) ∈
𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) |