Theorem hashbcss

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

	Ref	Expression
Hypothesis	ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
Assertion	hashbcss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 𝐶 𝑁 ) ⊆ ( 𝐴 𝐶 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		simp2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ⊆ 𝐴 )
3	2	sspwd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → 𝒫 𝐵 ⊆ 𝒫 𝐴 )
4		rabss2	⊢ ( 𝒫 𝐵 ⊆ 𝒫 𝐴 → { 𝑥 ∈ 𝒫 𝐵 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
5	3 4	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → { 𝑥 ∈ 𝒫 𝐵 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
6		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ 𝑉 )
7	6 2	ssexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ V )
8		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
9	1	hashbcval	⊢ ( ( 𝐵 ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐵 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
10	7 8 9	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐵 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
11	1	hashbcval	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
12	11	3adant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
13	5 10 12	3sstr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 𝐶 𝑁 ) ⊆ ( 𝐴 𝐶 𝑁 ) )