Theorem hashbcval

Description: Value of the "binomial set", the set of all N -element subsets of A . (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	hashbcval	|- ( ( A e. V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )
2		elex	|- ( A e. V -> A e. _V )
3		pwexg	|- ( A e. _V -> ~P A e. _V )
4	3	adantr	|- ( ( A e. _V /\ N e. NN0 ) -> ~P A e. _V )
5		rabexg	|- ( ~P A e. _V -> { x e. ~P A | ( # ` x ) = N } e. _V )
6	4 5	syl	|- ( ( A e. _V /\ N e. NN0 ) -> { x e. ~P A | ( # ` x ) = N } e. _V )
7		fveqeq2	|- ( b = x -> ( ( # ` b ) = i <-> ( # ` x ) = i ) )
8	7	cbvrabv	|- { b e. ~P a | ( # ` b ) = i } = { x e. ~P a | ( # ` x ) = i }
9		simpl	|- ( ( a = A /\ i = N ) -> a = A )
10	9	pweqd	|- ( ( a = A /\ i = N ) -> ~P a = ~P A )
11		simpr	|- ( ( a = A /\ i = N ) -> i = N )
12	11	eqeq2d	|- ( ( a = A /\ i = N ) -> ( ( # ` x ) = i <-> ( # ` x ) = N ) )
13	10 12	rabeqbidv	|- ( ( a = A /\ i = N ) -> { x e. ~P a | ( # ` x ) = i } = { x e. ~P A | ( # ` x ) = N } )
14	8 13	syl5eq	|- ( ( a = A /\ i = N ) -> { b e. ~P a | ( # ` b ) = i } = { x e. ~P A | ( # ` x ) = N } )
15	14 1	ovmpoga	|- ( ( A e. _V /\ N e. NN0 /\ { x e. ~P A | ( # ` x ) = N } e. _V ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )
16	6 15	mpd3an3	|- ( ( A e. _V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )
17	2 16	sylan	|- ( ( A e. V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )