Metamath Proof Explorer

Theorem sticksstones20

Description: Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024)

Ref Expression
Hypotheses sticksstones20.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones20.2 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
sticksstones20.3 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
sticksstones20.4 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
sticksstones20.5 ⊢ 𝐵 = { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) }
sticksstones20.6 ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = 𝐾 )
Assertion sticksstones20 ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ( 𝑁 + ( 𝐾 − 1 ) ) C ( 𝐾 − 1 ) ) )

Proof

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 ) ) )