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 )