Theorem hashbc2

Description: The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2	1	hashbcval	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
3	2	fveq2d	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝐴 𝐶 𝑁 ) ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ) )
4		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
5		hashbc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℤ ) → ( ( ♯ ‘ 𝐴 ) C 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ) )
6	4 5	sylan2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) C 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ) )
7	3 6	eqtr4d	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝐴 𝐶 𝑁 ) ) = ( ( ♯ ‘ 𝐴 ) C 𝑁 ) )