Step | Hyp | Ref
| Expression |
1 | | sticksstones20.2 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
2 | | isfinite4 13957 |
. . . . . . . 8
⊢ (𝑆 ∈ Fin ↔
(1...(♯‘𝑆))
≈ 𝑆) |
3 | | bren 8657 |
. . . . . . . 8
⊢
((1...(♯‘𝑆)) ≈ 𝑆 ↔ ∃𝑝 𝑝:(1...(♯‘𝑆))–1-1-onto→𝑆) |
4 | 2, 3 | sylbb 222 |
. . . . . . 7
⊢ (𝑆 ∈ Fin → ∃𝑝 𝑝:(1...(♯‘𝑆))–1-1-onto→𝑆) |
5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∃𝑝 𝑝:(1...(♯‘𝑆))–1-1-onto→𝑆) |
6 | | sticksstones20.6 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑆) = 𝐾) |
7 | 6 | oveq2d 7248 |
. . . . . . . . 9
⊢ (𝜑 → (1...(♯‘𝑆)) = (1...𝐾)) |
8 | 7 | f1oeq2d 6676 |
. . . . . . . 8
⊢ (𝜑 → (𝑝:(1...(♯‘𝑆))–1-1-onto→𝑆 ↔ 𝑝:(1...𝐾)–1-1-onto→𝑆)) |
9 | 8 | biimpd 232 |
. . . . . . 7
⊢ (𝜑 → (𝑝:(1...(♯‘𝑆))–1-1-onto→𝑆 → 𝑝:(1...𝐾)–1-1-onto→𝑆)) |
10 | 9 | eximdv 1925 |
. . . . . 6
⊢ (𝜑 → (∃𝑝 𝑝:(1...(♯‘𝑆))–1-1-onto→𝑆 → ∃𝑝 𝑝:(1...𝐾)–1-1-onto→𝑆)) |
11 | 5, 10 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑝 𝑝:(1...𝐾)–1-1-onto→𝑆) |
12 | | sticksstones20.4 |
. . . . . . . . . . 11
⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} |
13 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}) |
14 | | fzfid 13573 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝐾) ∈ Fin) |
15 | | nn0ex 12121 |
. . . . . . . . . . . . 13
⊢
ℕ0 ∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ0 ∈
V) |
17 | | mapex 8535 |
. . . . . . . . . . . 12
⊢
(((1...𝐾) ∈ Fin
∧ ℕ0 ∈ V) → {𝑔 ∣ 𝑔:(1...𝐾)⟶ℕ0} ∈
V) |
18 | 14, 16, 17 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑔 ∣ 𝑔:(1...𝐾)⟶ℕ0} ∈
V) |
19 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)) → 𝑔:(1...𝐾)⟶ℕ0) |
20 | 19 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁) → 𝑔:(1...𝐾)⟶ℕ0)) |
21 | 20 | ss2abdv 3992 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} ⊆ {𝑔 ∣ 𝑔:(1...𝐾)⟶ℕ0}) |
22 | 18, 21 | ssexd 5232 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} ∈ V) |
23 | 13, 22 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
24 | 23 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → 𝐴 ∈ V) |
25 | 24 | mptexd 7059 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑝‘𝑥)))) ∈ V) |
26 | | sticksstones20.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
27 | 26 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → 𝑁 ∈
ℕ0) |
28 | | sticksstones20.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℕ) |
29 | 28 | nnnn0d 12175 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
30 | 29 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → 𝐾 ∈
ℕ0) |
31 | | sticksstones20.5 |
. . . . . . . 8
⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} |
32 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → 𝑝:(1...𝐾)–1-1-onto→𝑆) |
33 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑝‘𝑥)))) = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑝‘𝑥)))) |
34 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑝‘𝑦)))) = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑝‘𝑦)))) |
35 | 27, 30, 12, 31, 32, 33, 34 | sticksstones19 39878 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑝‘𝑥)))):𝐴–1-1-onto→𝐵) |
36 | | f1oeq1 6668 |
. . . . . . 7
⊢ (𝑞 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑝‘𝑥)))) → (𝑞:𝐴–1-1-onto→𝐵 ↔ (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑝‘𝑥)))):𝐴–1-1-onto→𝐵)) |
37 | 25, 35, 36 | spcedv 3526 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → ∃𝑞 𝑞:𝐴–1-1-onto→𝐵) |
38 | | bren 8657 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑞 𝑞:𝐴–1-1-onto→𝐵) |
39 | 37, 38 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝:(1...𝐾)–1-1-onto→𝑆) → 𝐴 ≈ 𝐵) |
40 | 11, 39 | exlimddv 1943 |
. . . 4
⊢ (𝜑 → 𝐴 ≈ 𝐵) |
41 | | hasheni 13942 |
. . . 4
⊢ (𝐴 ≈ 𝐵 → (♯‘𝐴) = (♯‘𝐵)) |
42 | 40, 41 | syl 17 |
. . 3
⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) |
43 | 42 | eqcomd 2744 |
. 2
⊢ (𝜑 → (♯‘𝐵) = (♯‘𝐴)) |
44 | 26, 28, 12 | sticksstones16 39875 |
. 2
⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1))) |
45 | 43, 44 | eqtrd 2778 |
1
⊢ (𝜑 → (♯‘𝐵) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1))) |