Metamath Proof Explorer

Theorem hashbc2

Description: The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Hypothesis ramval.c 
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
Assertion hashbc2 
|- ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( ( # ` A ) _C N ) )

Proof

Step Hyp Ref Expression
1 ramval.c 
 |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2 1 hashbcval 
 |-  ( ( A e. Fin /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )
3 2 fveq2d 
 |-  ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( # ` { x e. ~P A | ( # ` x ) = N } ) )
4 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
5 hashbc 
 |-  ( ( A e. Fin /\ N e. ZZ ) -> ( ( # ` A ) _C N ) = ( # ` { x e. ~P A | ( # ` x ) = N } ) )
6 4 5 sylan2 
 |-  ( ( A e. Fin /\ N e. NN0 ) -> ( ( # ` A ) _C N ) = ( # ` { x e. ~P A | ( # ` x ) = N } ) )
7 3 6 eqtr4d 
 |-  ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( ( # ` A ) _C N ) )