hashbccl

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

		Ref	Expression
	Hypothesis	ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
	Assertion	hashbccl	$⊢ (A \in Fin \land N \in ℕ_{0}) \to A C N \in Fin$

Step	Hyp	Ref	Expression
1		ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2	1	hashbcval	$⊢ (A \in Fin \land N \in ℕ_{0}) \to A C N = \{x \in 𝒫 A \| \|x\| = N\}$
3		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
4	3	birani	$⊢ (A \in Fin \land N \in ℕ_{0}) \to 𝒫 A \in Fin$
5		ssrab2	$⊢ \{x \in 𝒫 A \| \|x\| = N\} \subseteq 𝒫 A$
6		ssfi	$⊢ (𝒫 A \in Fin \land \{x \in 𝒫 A \| \|x\| = N\} \subseteq 𝒫 A) \to \{x \in 𝒫 A \| \|x\| = N\} \in Fin$
7	4 5 6	sylancl	$⊢ (A \in Fin \land N \in ℕ_{0}) \to \{x \in 𝒫 A \| \|x\| = N\} \in Fin$
8	2 7	eqeltrd	$⊢ (A \in Fin \land N \in ℕ_{0}) \to A C N \in Fin$

Metamath Proof Explorer