# Metamath Proof Explorer

## Theorem hashbccl

Description: The binomial set is a finite set. (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 hashbccl
`|- ( ( A e. Fin /\ N e. NN0 ) -> ( A C N ) e. Fin )`

### 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 simpl
` |-  ( ( A e. Fin /\ N e. NN0 ) -> A e. Fin )`
4 pwfi
` |-  ( A e. Fin <-> ~P A e. Fin )`
5 3 4 sylib
` |-  ( ( A e. Fin /\ N e. NN0 ) -> ~P A e. Fin )`
6 ssrab2
` |-  { x e. ~P A | ( # ` x ) = N } C_ ~P A`
7 ssfi
` |-  ( ( ~P A e. Fin /\ { x e. ~P A | ( # ` x ) = N } C_ ~P A ) -> { x e. ~P A | ( # ` x ) = N } e. Fin )`
8 5 6 7 sylancl
` |-  ( ( A e. Fin /\ N e. NN0 ) -> { x e. ~P A | ( # ` x ) = N } e. Fin )`
9 2 8 eqeltrd
` |-  ( ( A e. Fin /\ N e. NN0 ) -> ( A C N ) e. Fin )`