Theorem hashbccl

Description: The binomial set is a finite set. (Contributed by Mario Carneiro, 20-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2	1	hashbcval	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } )
3		pwfi	⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
4	3	birani	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → 𝒫 𝐴 ∈ Fin )
5		ssrab2	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ⊆ 𝒫 𝐴
6		ssfi	⊢ ( ( 𝒫 𝐴 ∈ Fin ∧ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ⊆ 𝒫 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ∈ Fin )
7	4 5 6	sylancl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝑁 } ∈ Fin )
8	2 7	eqeltrd	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 𝐶 𝑁 ) ∈ Fin )