| Step | Hyp | Ref
| Expression |
| 1 | | hashgval2 14417 |
. . . 4
⊢ (♯
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
| 2 | 1 | hashgf1o 14012 |
. . 3
⊢ (♯
↾ ω):ω–1-1-onto→ℕ0 |
| 3 | | sneq 4636 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → {𝑤} = {𝑦}) |
| 4 | | pweq 4614 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → 𝒫 𝑤 = 𝒫 𝑦) |
| 5 | 3, 4 | xpeq12d 5716 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ({𝑤} × 𝒫 𝑤) = ({𝑦} × 𝒫 𝑦)) |
| 6 | 5 | cbviunv 5040 |
. . . . . . . 8
⊢ ∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤) = ∪ 𝑦 ∈ 𝑧 ({𝑦} × 𝒫 𝑦) |
| 7 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ∪
𝑦 ∈ 𝑧 ({𝑦} × 𝒫 𝑦) = ∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)) |
| 8 | 6, 7 | eqtrid 2789 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ∪
𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤) = ∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)) |
| 9 | 8 | fveq2d 6910 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)) = (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
| 10 | 9 | cbvmptv 5255 |
. . . . 5
⊢ (𝑧 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
| 11 | 10 | ackbij1 10277 |
. . . 4
⊢ (𝑧 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))):(𝒫 ω ∩ Fin)–1-1-onto→ω |
| 12 | | f1ocnv 6860 |
. . . . . 6
⊢ ((♯
↾ ω):ω–1-1-onto→ℕ0 → ◡(♯ ↾
ω):ℕ0–1-1-onto→ω) |
| 13 | 2, 12 | ax-mp 5 |
. . . . 5
⊢ ◡(♯ ↾
ω):ℕ0–1-1-onto→ω |
| 14 | | f1opwfi 9396 |
. . . . 5
⊢ (◡(♯ ↾
ω):ℕ0–1-1-onto→ω → (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)):(𝒫 ℕ0 ∩
Fin)–1-1-onto→(𝒫 ω ∩
Fin)) |
| 15 | 13, 14 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)):(𝒫
ℕ0 ∩ Fin)–1-1-onto→(𝒫 ω ∩ Fin) |
| 16 | | f1oco 6871 |
. . . 4
⊢ (((𝑧 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))):(𝒫 ω ∩ Fin)–1-1-onto→ω ∧ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)):(𝒫 ℕ0 ∩
Fin)–1-1-onto→(𝒫 ω ∩ Fin)) → ((𝑧 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ω) |
| 17 | 11, 15, 16 | mp2an 692 |
. . 3
⊢ ((𝑧 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ω |
| 18 | | f1oco 6871 |
. . 3
⊢
(((♯ ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ω) → ((♯ ↾ ω)
∘ ((𝑧 ∈
(𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0) |
| 19 | 2, 17, 18 | mp2an 692 |
. 2
⊢ ((♯
↾ ω) ∘ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 |
| 20 | | inss2 4238 |
. . . . . . . . . 10
⊢
(𝒫 ω ∩ Fin) ⊆ Fin |
| 21 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)):(𝒫
ℕ0 ∩ Fin)–1-1-onto→(𝒫 ω ∩ Fin) → (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)):(𝒫
ℕ0 ∩ Fin)⟶(𝒫 ω ∩
Fin)) |
| 22 | 15, 21 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)):(𝒫
ℕ0 ∩ Fin)⟶(𝒫 ω ∩
Fin) |
| 23 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)) = (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)) |
| 24 | 23 | fmpt 7130 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝒫 ℕ0 ∩ Fin)(◡(♯ ↾ ω) “ 𝑥) ∈ (𝒫 ω
∩ Fin) ↔ (𝑥 ∈
(𝒫 ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)):(𝒫
ℕ0 ∩ Fin)⟶(𝒫 ω ∩
Fin)) |
| 25 | 22, 24 | mpbir 231 |
. . . . . . . . . . 11
⊢
∀𝑥 ∈
(𝒫 ℕ0 ∩ Fin)(◡(♯ ↾ ω) “ 𝑥) ∈ (𝒫 ω
∩ Fin) |
| 26 | 25 | rspec 3250 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (◡(♯ ↾ ω) “ 𝑥) ∈ (𝒫 ω
∩ Fin)) |
| 27 | 20, 26 | sselid 3981 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (◡(♯ ↾ ω) “ 𝑥) ∈ Fin) |
| 28 | | snfi 9083 |
. . . . . . . . . . 11
⊢ {𝑤} ∈ Fin |
| 29 | | cnvimass 6100 |
. . . . . . . . . . . . . . 15
⊢ (◡(♯ ↾ ω) “ 𝑥) ⊆ dom (♯ ↾
ω) |
| 30 | | dmhashres 14380 |
. . . . . . . . . . . . . . 15
⊢ dom
(♯ ↾ ω) = ω |
| 31 | 29, 30 | sseqtri 4032 |
. . . . . . . . . . . . . 14
⊢ (◡(♯ ↾ ω) “ 𝑥) ⊆
ω |
| 32 | | onfin2 9268 |
. . . . . . . . . . . . . . 15
⊢ ω =
(On ∩ Fin) |
| 33 | | inss2 4238 |
. . . . . . . . . . . . . . 15
⊢ (On ∩
Fin) ⊆ Fin |
| 34 | 32, 33 | eqsstri 4030 |
. . . . . . . . . . . . . 14
⊢ ω
⊆ Fin |
| 35 | 31, 34 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ (◡(♯ ↾ ω) “ 𝑥) ⊆ Fin |
| 36 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)) → 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)) |
| 37 | 35, 36 | sselid 3981 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)) → 𝑤 ∈ Fin) |
| 38 | | pwfi 9357 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ Fin ↔ 𝒫
𝑤 ∈
Fin) |
| 39 | 37, 38 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)) → 𝒫 𝑤 ∈ Fin) |
| 40 | | xpfi 9358 |
. . . . . . . . . . 11
⊢ (({𝑤} ∈ Fin ∧ 𝒫
𝑤 ∈ Fin) →
({𝑤} × 𝒫
𝑤) ∈
Fin) |
| 41 | 28, 39, 40 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)) → ({𝑤} × 𝒫 𝑤) ∈ Fin) |
| 42 | 41 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → ∀𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤) ∈ Fin) |
| 43 | | iunfi 9383 |
. . . . . . . . 9
⊢ (((◡(♯ ↾ ω) “ 𝑥) ∈ Fin ∧ ∀𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤) ∈ Fin) → ∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤) ∈ Fin) |
| 44 | 27, 42, 43 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → ∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤) ∈ Fin) |
| 45 | | ficardom 10001 |
. . . . . . . 8
⊢ (∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤) ∈ Fin → (card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) ∈ ω) |
| 46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) ∈ ω) |
| 47 | 46 | fvresd 6926 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → ((♯ ↾
ω)‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) = (♯‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)))) |
| 48 | | hashcard 14394 |
. . . . . . 7
⊢ (∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤) ∈ Fin →
(♯‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) = (♯‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) |
| 49 | 44, 48 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (♯‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) = (♯‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) |
| 50 | | xp1st 8046 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑤} × 𝒫 𝑤) → (1st ‘𝑧) ∈ {𝑤}) |
| 51 | | elsni 4643 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧) ∈ {𝑤} → (1st ‘𝑧) = 𝑤) |
| 52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑤} × 𝒫 𝑤) → (1st ‘𝑧) = 𝑤) |
| 53 | 52 | rgen 3063 |
. . . . . . . . . 10
⊢
∀𝑧 ∈
({𝑤} × 𝒫
𝑤)(1st
‘𝑧) = 𝑤 |
| 54 | 53 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑤 ∈
(◡(♯ ↾ ω) “
𝑥)∀𝑧 ∈ ({𝑤} × 𝒫 𝑤)(1st ‘𝑧) = 𝑤 |
| 55 | | invdisj 5129 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
(◡(♯ ↾ ω) “
𝑥)∀𝑧 ∈ ({𝑤} × 𝒫 𝑤)(1st ‘𝑧) = 𝑤 → Disj 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) |
| 56 | 54, 55 | mp1i 13 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → Disj 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) |
| 57 | 27, 41, 56 | hashiun 15858 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (♯‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) = Σ𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)(♯‘({𝑤} × 𝒫 𝑤))) |
| 58 | | sneq 4636 |
. . . . . . . . . 10
⊢ (𝑤 = (◡(♯ ↾ ω)‘𝑦) → {𝑤} = {(◡(♯ ↾ ω)‘𝑦)}) |
| 59 | | pweq 4614 |
. . . . . . . . . 10
⊢ (𝑤 = (◡(♯ ↾ ω)‘𝑦) → 𝒫 𝑤 = 𝒫 (◡(♯ ↾ ω)‘𝑦)) |
| 60 | 58, 59 | xpeq12d 5716 |
. . . . . . . . 9
⊢ (𝑤 = (◡(♯ ↾ ω)‘𝑦) → ({𝑤} × 𝒫 𝑤) = ({(◡(♯ ↾ ω)‘𝑦)} × 𝒫 (◡(♯ ↾ ω)‘𝑦))) |
| 61 | 60 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑤 = (◡(♯ ↾ ω)‘𝑦) → (♯‘({𝑤} × 𝒫 𝑤)) = (♯‘({(◡(♯ ↾ ω)‘𝑦)} × 𝒫 (◡(♯ ↾ ω)‘𝑦)))) |
| 62 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → 𝑥 ∈ Fin) |
| 63 | | f1of1 6847 |
. . . . . . . . . 10
⊢ (◡(♯ ↾
ω):ℕ0–1-1-onto→ω → ◡(♯ ↾
ω):ℕ0–1-1→ω) |
| 64 | 13, 63 | ax-mp 5 |
. . . . . . . . 9
⊢ ◡(♯ ↾
ω):ℕ0–1-1→ω |
| 65 | | elinel1 4201 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → 𝑥 ∈ 𝒫
ℕ0) |
| 66 | 65 | elpwid 4609 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → 𝑥 ⊆
ℕ0) |
| 67 | | f1ores 6862 |
. . . . . . . . 9
⊢ ((◡(♯ ↾
ω):ℕ0–1-1→ω ∧ 𝑥 ⊆ ℕ0) → (◡(♯ ↾ ω) ↾ 𝑥):𝑥–1-1-onto→(◡(♯ ↾ ω) “ 𝑥)) |
| 68 | 64, 66, 67 | sylancr 587 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (◡(♯ ↾ ω) ↾ 𝑥):𝑥–1-1-onto→(◡(♯ ↾ ω) “ 𝑥)) |
| 69 | | fvres 6925 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑥 → ((◡(♯ ↾ ω) ↾ 𝑥)‘𝑦) = (◡(♯ ↾ ω)‘𝑦)) |
| 70 | 69 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((◡(♯ ↾ ω) ↾ 𝑥)‘𝑦) = (◡(♯ ↾ ω)‘𝑦)) |
| 71 | | hashcl 14395 |
. . . . . . . . 9
⊢ (({𝑤} × 𝒫 𝑤) ∈ Fin →
(♯‘({𝑤} ×
𝒫 𝑤)) ∈
ℕ0) |
| 72 | | nn0cn 12536 |
. . . . . . . . 9
⊢
((♯‘({𝑤}
× 𝒫 𝑤))
∈ ℕ0 → (♯‘({𝑤} × 𝒫 𝑤)) ∈ ℂ) |
| 73 | 41, 71, 72 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)) → (♯‘({𝑤} × 𝒫 𝑤)) ∈
ℂ) |
| 74 | 61, 62, 68, 70, 73 | fsumf1o 15759 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)(♯‘({𝑤} × 𝒫 𝑤)) = Σ𝑦 ∈ 𝑥 (♯‘({(◡(♯ ↾ ω)‘𝑦)} × 𝒫 (◡(♯ ↾ ω)‘𝑦)))) |
| 75 | | snfi 9083 |
. . . . . . . . . 10
⊢ {(◡(♯ ↾ ω)‘𝑦)} ∈ Fin |
| 76 | 66 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℕ0) |
| 77 | | f1of 6848 |
. . . . . . . . . . . . . . 15
⊢ (◡(♯ ↾
ω):ℕ0–1-1-onto→ω → ◡(♯ ↾
ω):ℕ0⟶ω) |
| 78 | 13, 77 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ◡(♯ ↾
ω):ℕ0⟶ω |
| 79 | 78 | ffvelcdmi 7103 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ (◡(♯ ↾
ω)‘𝑦) ∈
ω) |
| 80 | 76, 79 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (◡(♯ ↾ ω)‘𝑦) ∈
ω) |
| 81 | 34, 80 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (◡(♯ ↾ ω)‘𝑦) ∈ Fin) |
| 82 | | pwfi 9357 |
. . . . . . . . . . 11
⊢ ((◡(♯ ↾ ω)‘𝑦) ∈ Fin ↔ 𝒫
(◡(♯ ↾ ω)‘𝑦) ∈ Fin) |
| 83 | 81, 82 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝒫 (◡(♯ ↾ ω)‘𝑦) ∈ Fin) |
| 84 | | hashxp 14473 |
. . . . . . . . . 10
⊢ (({(◡(♯ ↾ ω)‘𝑦)} ∈ Fin ∧ 𝒫
(◡(♯ ↾ ω)‘𝑦) ∈ Fin) →
(♯‘({(◡(♯ ↾
ω)‘𝑦)} ×
𝒫 (◡(♯ ↾
ω)‘𝑦))) =
((♯‘{(◡(♯ ↾
ω)‘𝑦)})
· (♯‘𝒫 (◡(♯ ↾ ω)‘𝑦)))) |
| 85 | 75, 83, 84 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (♯‘({(◡(♯ ↾ ω)‘𝑦)} × 𝒫 (◡(♯ ↾ ω)‘𝑦))) = ((♯‘{(◡(♯ ↾ ω)‘𝑦)}) ·
(♯‘𝒫 (◡(♯
↾ ω)‘𝑦)))) |
| 86 | | hashsng 14408 |
. . . . . . . . . . 11
⊢ ((◡(♯ ↾ ω)‘𝑦) ∈ ω →
(♯‘{(◡(♯ ↾
ω)‘𝑦)}) =
1) |
| 87 | 80, 86 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (♯‘{(◡(♯ ↾ ω)‘𝑦)}) = 1) |
| 88 | | hashpw 14475 |
. . . . . . . . . . . 12
⊢ ((◡(♯ ↾ ω)‘𝑦) ∈ Fin →
(♯‘𝒫 (◡(♯
↾ ω)‘𝑦))
= (2↑(♯‘(◡(♯
↾ ω)‘𝑦)))) |
| 89 | 81, 88 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (♯‘𝒫 (◡(♯ ↾ ω)‘𝑦)) =
(2↑(♯‘(◡(♯
↾ ω)‘𝑦)))) |
| 90 | 80 | fvresd 6926 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((♯ ↾
ω)‘(◡(♯ ↾
ω)‘𝑦)) =
(♯‘(◡(♯ ↾
ω)‘𝑦))) |
| 91 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . 14
⊢
(((♯ ↾ ω):ω–1-1-onto→ℕ0 ∧ 𝑦 ∈ ℕ0) → ((♯
↾ ω)‘(◡(♯
↾ ω)‘𝑦))
= 𝑦) |
| 92 | 2, 76, 91 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((♯ ↾
ω)‘(◡(♯ ↾
ω)‘𝑦)) = 𝑦) |
| 93 | 90, 92 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (♯‘(◡(♯ ↾ ω)‘𝑦)) = 𝑦) |
| 94 | 93 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (2↑(♯‘(◡(♯ ↾ ω)‘𝑦))) = (2↑𝑦)) |
| 95 | 89, 94 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (♯‘𝒫 (◡(♯ ↾ ω)‘𝑦)) = (2↑𝑦)) |
| 96 | 87, 95 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((♯‘{(◡(♯ ↾ ω)‘𝑦)}) ·
(♯‘𝒫 (◡(♯
↾ ω)‘𝑦)))
= (1 · (2↑𝑦))) |
| 97 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 98 | | expcl 14120 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑦
∈ ℕ0) → (2↑𝑦) ∈ ℂ) |
| 99 | 97, 76, 98 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (2↑𝑦) ∈ ℂ) |
| 100 | 99 | mullidd 11279 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (1 · (2↑𝑦)) = (2↑𝑦)) |
| 101 | 85, 96, 100 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (♯‘({(◡(♯ ↾ ω)‘𝑦)} × 𝒫 (◡(♯ ↾ ω)‘𝑦))) = (2↑𝑦)) |
| 102 | 101 | sumeq2dv 15738 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → Σ𝑦 ∈ 𝑥 (♯‘({(◡(♯ ↾ ω)‘𝑦)} × 𝒫 (◡(♯ ↾ ω)‘𝑦))) = Σ𝑦 ∈ 𝑥 (2↑𝑦)) |
| 103 | 57, 74, 102 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → (♯‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) = Σ𝑦 ∈ 𝑥 (2↑𝑦)) |
| 104 | 47, 49, 103 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) → ((♯ ↾
ω)‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) = Σ𝑦 ∈ 𝑥 (2↑𝑦)) |
| 105 | 104 | mpteq2ia 5245 |
. . . 4
⊢ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ ((♯ ↾
ω)‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)))) = (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑦
∈ 𝑥 (2↑𝑦)) |
| 106 | 46 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (𝒫 ℕ0 ∩ Fin)) → (card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) ∈ ω) |
| 107 | 26 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (𝒫 ℕ0 ∩ Fin)) → (◡(♯ ↾ ω) “ 𝑥) ∈ (𝒫 ω
∩ Fin)) |
| 108 | | eqidd 2738 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (◡(♯ ↾ ω) “ 𝑥)) = (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥))) |
| 109 | | eqidd 2738 |
. . . . . . 7
⊢ (⊤
→ (𝑧 ∈ (𝒫
ω ∩ Fin) ↦ (card‘∪
𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) = (𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)))) |
| 110 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑧 = (◡(♯ ↾ ω) “ 𝑥) → ∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤) = ∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) |
| 111 | 110 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑧 = (◡(♯ ↾ ω) “ 𝑥) → (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤)) = (card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))) |
| 112 | 107, 108,
109, 111 | fmptco 7149 |
. . . . . 6
⊢ (⊤
→ ((𝑧 ∈
(𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥))) =
(𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ (card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)))) |
| 113 | | f1of 6848 |
. . . . . . . 8
⊢ ((♯
↾ ω):ω–1-1-onto→ℕ0 → (♯
↾ ω):ω⟶ℕ0) |
| 114 | 2, 113 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ (♯ ↾
ω):ω⟶ℕ0) |
| 115 | 114 | feqmptd 6977 |
. . . . . 6
⊢ (⊤
→ (♯ ↾ ω) = (𝑦 ∈ ω ↦ ((♯ ↾
ω)‘𝑦))) |
| 116 | | fveq2 6906 |
. . . . . 6
⊢ (𝑦 = (card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)) → ((♯ ↾
ω)‘𝑦) =
((♯ ↾ ω)‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)))) |
| 117 | 106, 112,
115, 116 | fmptco 7149 |
. . . . 5
⊢ (⊤
→ ((♯ ↾ ω) ∘ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))) =
(𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ ((♯ ↾
ω)‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤))))) |
| 118 | 117 | mptru 1547 |
. . . 4
⊢ ((♯
↾ ω) ∘ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))) =
(𝑥 ∈ (𝒫
ℕ0 ∩ Fin) ↦ ((♯ ↾
ω)‘(card‘∪ 𝑤 ∈ (◡(♯ ↾ ω) “ 𝑥)({𝑤} × 𝒫 𝑤)))) |
| 119 | | ackbijnn.1 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ Σ𝑦
∈ 𝑥 (2↑𝑦)) |
| 120 | 105, 118,
119 | 3eqtr4i 2775 |
. . 3
⊢ ((♯
↾ ω) ∘ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))) =
𝐹 |
| 121 | | f1oeq1 6836 |
. . 3
⊢
(((♯ ↾ ω) ∘ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))) =
𝐹 → (((♯ ↾
ω) ∘ ((𝑧 ∈
(𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 ↔ 𝐹:(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0)) |
| 122 | 120, 121 | ax-mp 5 |
. 2
⊢
(((♯ ↾ ω) ∘ ((𝑧 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑤 ∈ 𝑧 ({𝑤} × 𝒫 𝑤))) ∘ (𝑥 ∈ (𝒫 ℕ0 ∩
Fin) ↦ (◡(♯ ↾
ω) “ 𝑥)))):(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0 ↔ 𝐹:(𝒫 ℕ0 ∩
Fin)–1-1-onto→ℕ0) |
| 123 | 19, 122 | mpbi 230 |
1
⊢ 𝐹:(𝒫 ℕ0
∩ Fin)–1-1-onto→ℕ0 |