0hashbc

Description: There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015)

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

Step	Hyp	Ref	Expression
1		ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2		0fin	$⊢ \emptyset \in Fin$
3		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
4	1	hashbc2	$⊢ (\emptyset \in Fin \land N \in ℕ_{0}) \to \|\emptyset C N\| = (\binom{\|\emptyset\|}{N})$
5	2 3 4	sylancr	$⊢ N \in ℕ \to \|\emptyset C N\| = (\binom{\|\emptyset\|}{N})$
6		hash0	$⊢ \|\emptyset\| = 0$
7	6	oveq1i	$⊢ (\binom{\|\emptyset\|}{N}) = (\binom{0}{N})$
8		bc0k	$⊢ N \in ℕ \to (\binom{0}{N}) = 0$
9	7 8	eqtrid	$⊢ N \in ℕ \to (\binom{\|\emptyset\|}{N}) = 0$
10	5 9	eqtrd	$⊢ N \in ℕ \to \|\emptyset C N\| = 0$
11		ovex	$⊢ \emptyset C N \in V$
12		hasheq0	$⊢ \emptyset C N \in V \to (\|\emptyset C N\| = 0 \leftrightarrow \emptyset C N = \emptyset)$
13	11 12	ax-mp	$⊢ \|\emptyset C N\| = 0 \leftrightarrow \emptyset C N = \emptyset$
14	10 13	sylib	$⊢ N \in ℕ \to \emptyset C N = \emptyset$

Metamath Proof Explorer