Proof of Theorem dfac12k
| Step | Hyp | Ref
| Expression |
| 1 | | alephon 10109 |
. . . 4
⊢
(ℵ‘𝑦)
∈ On |
| 2 | | pweq 4614 |
. . . . . 6
⊢ (𝑥 = (ℵ‘𝑦) → 𝒫 𝑥 = 𝒫
(ℵ‘𝑦)) |
| 3 | 2 | eleq1d 2826 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝑦) → (𝒫 𝑥 ∈ dom card ↔
𝒫 (ℵ‘𝑦)
∈ dom card)) |
| 4 | 3 | rspcv 3618 |
. . . 4
⊢
((ℵ‘𝑦)
∈ On → (∀𝑥
∈ On 𝒫 𝑥
∈ dom card → 𝒫 (ℵ‘𝑦) ∈ dom card)) |
| 5 | 1, 4 | ax-mp 5 |
. . 3
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ 𝒫 (ℵ‘𝑦) ∈ dom card) |
| 6 | 5 | ralrimivw 3150 |
. 2
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ ∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card) |
| 7 | | omelon 9686 |
. . . . . . 7
⊢ ω
∈ On |
| 8 | | cardon 9984 |
. . . . . . 7
⊢
(card‘𝑥)
∈ On |
| 9 | | ontri1 6418 |
. . . . . . 7
⊢ ((ω
∈ On ∧ (card‘𝑥) ∈ On) → (ω ⊆
(card‘𝑥) ↔ ¬
(card‘𝑥) ∈
ω)) |
| 10 | 7, 8, 9 | mp2an 692 |
. . . . . 6
⊢ (ω
⊆ (card‘𝑥)
↔ ¬ (card‘𝑥)
∈ ω) |
| 11 | | cardidm 9999 |
. . . . . . . 8
⊢
(card‘(card‘𝑥)) = (card‘𝑥) |
| 12 | | cardalephex 10130 |
. . . . . . . 8
⊢ (ω
⊆ (card‘𝑥)
→ ((card‘(card‘𝑥)) = (card‘𝑥) ↔ ∃𝑦 ∈ On (card‘𝑥) = (ℵ‘𝑦))) |
| 13 | 11, 12 | mpbii 233 |
. . . . . . 7
⊢ (ω
⊆ (card‘𝑥)
→ ∃𝑦 ∈ On
(card‘𝑥) =
(ℵ‘𝑦)) |
| 14 | | r19.29 3114 |
. . . . . . . . 9
⊢
((∀𝑦 ∈
On 𝒫 (ℵ‘𝑦) ∈ dom card ∧ ∃𝑦 ∈ On (card‘𝑥) = (ℵ‘𝑦)) → ∃𝑦 ∈ On (𝒫
(ℵ‘𝑦) ∈
dom card ∧ (card‘𝑥) = (ℵ‘𝑦))) |
| 15 | | pweq 4614 |
. . . . . . . . . . . 12
⊢
((card‘𝑥) =
(ℵ‘𝑦) →
𝒫 (card‘𝑥) =
𝒫 (ℵ‘𝑦)) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . 11
⊢
((card‘𝑥) =
(ℵ‘𝑦) →
(𝒫 (card‘𝑥)
∈ dom card ↔ 𝒫 (ℵ‘𝑦) ∈ dom card)) |
| 17 | 16 | biimparc 479 |
. . . . . . . . . 10
⊢
((𝒫 (ℵ‘𝑦) ∈ dom card ∧ (card‘𝑥) = (ℵ‘𝑦)) → 𝒫
(card‘𝑥) ∈ dom
card) |
| 18 | 17 | rexlimivw 3151 |
. . . . . . . . 9
⊢
(∃𝑦 ∈ On
(𝒫 (ℵ‘𝑦) ∈ dom card ∧ (card‘𝑥) = (ℵ‘𝑦)) → 𝒫
(card‘𝑥) ∈ dom
card) |
| 19 | 14, 18 | syl 17 |
. . . . . . . 8
⊢
((∀𝑦 ∈
On 𝒫 (ℵ‘𝑦) ∈ dom card ∧ ∃𝑦 ∈ On (card‘𝑥) = (ℵ‘𝑦)) → 𝒫
(card‘𝑥) ∈ dom
card) |
| 20 | 19 | ex 412 |
. . . . . . 7
⊢
(∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card → (∃𝑦 ∈ On (card‘𝑥) = (ℵ‘𝑦) → 𝒫 (card‘𝑥) ∈ dom
card)) |
| 21 | 13, 20 | syl5 34 |
. . . . . 6
⊢
(∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card → (ω ⊆ (card‘𝑥) → 𝒫 (card‘𝑥) ∈ dom
card)) |
| 22 | 10, 21 | biimtrrid 243 |
. . . . 5
⊢
(∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card → (¬ (card‘𝑥) ∈ ω → 𝒫
(card‘𝑥) ∈ dom
card)) |
| 23 | | nnfi 9207 |
. . . . . . 7
⊢
((card‘𝑥)
∈ ω → (card‘𝑥) ∈ Fin) |
| 24 | | pwfi 9357 |
. . . . . . 7
⊢
((card‘𝑥)
∈ Fin ↔ 𝒫 (card‘𝑥) ∈ Fin) |
| 25 | 23, 24 | sylib 218 |
. . . . . 6
⊢
((card‘𝑥)
∈ ω → 𝒫 (card‘𝑥) ∈ Fin) |
| 26 | | finnum 9988 |
. . . . . 6
⊢
(𝒫 (card‘𝑥) ∈ Fin → 𝒫
(card‘𝑥) ∈ dom
card) |
| 27 | 25, 26 | syl 17 |
. . . . 5
⊢
((card‘𝑥)
∈ ω → 𝒫 (card‘𝑥) ∈ dom card) |
| 28 | 22, 27 | pm2.61d2 181 |
. . . 4
⊢
(∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card → 𝒫 (card‘𝑥) ∈ dom card) |
| 29 | | oncardid 9996 |
. . . . 5
⊢ (𝑥 ∈ On →
(card‘𝑥) ≈
𝑥) |
| 30 | | pwen 9190 |
. . . . 5
⊢
((card‘𝑥)
≈ 𝑥 → 𝒫
(card‘𝑥) ≈
𝒫 𝑥) |
| 31 | | ennum 9987 |
. . . . 5
⊢
(𝒫 (card‘𝑥) ≈ 𝒫 𝑥 → (𝒫 (card‘𝑥) ∈ dom card ↔
𝒫 𝑥 ∈ dom
card)) |
| 32 | 29, 30, 31 | 3syl 18 |
. . . 4
⊢ (𝑥 ∈ On → (𝒫
(card‘𝑥) ∈ dom
card ↔ 𝒫 𝑥
∈ dom card)) |
| 33 | 28, 32 | syl5ibcom 245 |
. . 3
⊢
(∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card → (𝑥
∈ On → 𝒫 𝑥 ∈ dom card)) |
| 34 | 33 | ralrimiv 3145 |
. 2
⊢
(∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card → ∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card) |
| 35 | 6, 34 | impbii 209 |
1
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
↔ ∀𝑦 ∈ On
𝒫 (ℵ‘𝑦)
∈ dom card) |