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		simpl	$⊢ (A \in Fin \land N \in ℕ_{0}) \to A \in Fin$
4		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
5	3 4	sylib	$⊢ (A \in Fin \land N \in ℕ_{0}) \to 𝒫 A \in Fin$
6		ssrab2	$⊢ \{x \in 𝒫 A \| \|x\| = N\} \subseteq 𝒫 A$
7		ssfi	$⊢ (𝒫 A \in Fin \land \{x \in 𝒫 A \| \|x\| = N\} \subseteq 𝒫 A) \to \{x \in 𝒫 A \| \|x\| = N\} \in Fin$
8	5 6 7	sylancl	$⊢ (A \in Fin \land N \in ℕ_{0}) \to \{x \in 𝒫 A \| \|x\| = N\} \in Fin$
9	2 8	eqeltrd	$⊢ (A \in Fin \land N \in ℕ_{0}) \to A C N \in Fin$

Metamath Proof Explorer