Theorem hashbcss

Description: Subset relation for the binomial set. (Contributed by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Hypothesis	ramval.c	$$⊢C=\left(a\in \mathrm{V},i\in {\mathbb{N}}_0⟼\left\{b\in 𝒫a|\left|b\right|=i\right\}\right)$$
Assertion	hashbcss	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to BCN\subseteq ACN$$

Proof

Step	Hyp	Ref	Expression
1		ramval.c	$$⊢C=\left(a\in \mathrm{V},i\in {\mathbb{N}}_0⟼\left\{b\in 𝒫a|\left|b\right|=i\right\}\right)$$
2		simp2	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to B\subseteq A$$
3	2	sspwd	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to 𝒫B\subseteq 𝒫A$$
4		rabss2	$$⊢𝒫B\subseteq 𝒫A\to \left\{x\in 𝒫B|\left|x\right|=N\right\}\subseteq \left\{x\in 𝒫A|\left|x\right|=N\right\}$$
5	3 4	syl	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to \left\{x\in 𝒫B|\left|x\right|=N\right\}\subseteq \left\{x\in 𝒫A|\left|x\right|=N\right\}$$
6		simp1	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to A\in V$$
7	6 2	ssexd	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to B\in \mathrm{V}$$
8		simp3	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
9	1	hashbcval	$$⊢\left(B\in \mathrm{V}\wedge N\in {\mathbb{N}}_0\right)\to BCN=\left\{x\in 𝒫B|\left|x\right|=N\right\}$$
10	7 8 9	syl2anc	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to BCN=\left\{x\in 𝒫B|\left|x\right|=N\right\}$$
11	1	hashbcval	$$⊢\left(A\in V\wedge N\in {\mathbb{N}}_0\right)\to ACN=\left\{x\in 𝒫A|\left|x\right|=N\right\}$$
12	11	3adant2	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to ACN=\left\{x\in 𝒫A|\left|x\right|=N\right\}$$
13	5 10 12	3sstr4d	$$⊢\left(A\in V\wedge B\subseteq A\wedge N\in {\mathbb{N}}_0\right)\to BCN\subseteq ACN$$