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