Theorem hashbcss

Description: Subset relation for the binomial 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	hashbcss	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> ( B C N ) C_ ( 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		simp2	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> B C_ A )
3	2	sspwd	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> ~P B C_ ~P A )
4		rabss2	|- ( ~P B C_ ~P A -> { x e. ~P B | ( # ` x ) = N } C_ { x e. ~P A | ( # ` x ) = N } )
5	3 4	syl	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> { x e. ~P B | ( # ` x ) = N } C_ { x e. ~P A | ( # ` x ) = N } )
6		simp1	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> A e. V )
7	6 2	ssexd	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> B e. _V )
8		simp3	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> N e. NN0 )
9	1	hashbcval	|- ( ( B e. _V /\ N e. NN0 ) -> ( B C N ) = { x e. ~P B | ( # ` x ) = N } )
10	7 8 9	syl2anc	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> ( B C N ) = { x e. ~P B | ( # ` x ) = N } )
11	1	hashbcval	|- ( ( A e. V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )
12	11	3adant2	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )
13	5 10 12	3sstr4d	|- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> ( B C N ) C_ ( A C N ) )