Metamath Proof Explorer

Theorem sticksstones23

Description: Non-exhaustive sticks and stones. (Contributed by metakunt, 7-May-2025)

Ref Expression
Hypotheses sticksstones23.1 
|- ( ph -> N e. NN0 )
sticksstones23.2 
|- ( ph -> S e. Fin )
sticksstones23.3 
|- ( ph -> S =/= (/) )
sticksstones23.4 
|- A = { f e. ( NN0 ^m S ) | sum_ i e. S ( f ` i ) <_ N }
Assertion sticksstones23 
|- ( ph -> ( # ` A ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones23.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones23.2 
 |-  ( ph -> S e. Fin )
3 sticksstones23.3 
 |-  ( ph -> S =/= (/) )
4 sticksstones23.4 
 |-  A = { f e. ( NN0 ^m S ) | sum_ i e. S ( f ` i ) <_ N }
5 4 a1i 
 |-  ( ph -> A = { f e. ( NN0 ^m S ) | sum_ i e. S ( f ` i ) <_ N } )
6 df-rab 
 |-  { f e. ( NN0 ^m S ) | sum_ i e. S ( f ` i ) <_ N } = { f | ( f e. ( NN0 ^m S ) /\ sum_ i e. S ( f ` i ) <_ N ) }
7 6 a1i 
 |-  ( ph -> { f e. ( NN0 ^m S ) | sum_ i e. S ( f ` i ) <_ N } = { f | ( f e. ( NN0 ^m S ) /\ sum_ i e. S ( f ` i ) <_ N ) } )
8 nn0ex 
 |-  NN0 e. _V
9 8 a1i 
 |-  ( ph -> NN0 e. _V )
10 elmapg 
 |-  ( ( NN0 e. _V /\ S e. Fin ) -> ( f e. ( NN0 ^m S ) <-> f : S --> NN0 ) )
11 9 2 10 syl2anc 
 |-  ( ph -> ( f e. ( NN0 ^m S ) <-> f : S --> NN0 ) )
12 11 anbi1d 
 |-  ( ph -> ( ( f e. ( NN0 ^m S ) /\ sum_ i e. S ( f ` i ) <_ N ) <-> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) ) )
13 12 abbidv 
 |-  ( ph -> { f | ( f e. ( NN0 ^m S ) /\ sum_ i e. S ( f ` i ) <_ N ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } )
14 7 13 eqtrd 
 |-  ( ph -> { f e. ( NN0 ^m S ) | sum_ i e. S ( f ` i ) <_ N } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } )
15 5 14 eqtrd 
 |-  ( ph -> A = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } )
16 15 fveq2d 
 |-  ( ph -> ( # ` A ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) )
17 eqid 
 |-  { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) }
18 1 2 3 17 sticksstones22 
 |-  ( ph -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )
19 16 18 eqtrd 
 |-  ( ph -> ( # ` A ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )