Theorem 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	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
Assertion	0hashbc	⊢ ( 𝑁 ∈ ℕ → ( ∅ 𝐶 𝑁 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ramval.c	⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2		0fin	⊢ ∅ ∈ Fin
3		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4	1	hashbc2	⊢ ( ( ∅ ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( ∅ 𝐶 𝑁 ) ) = ( ( ♯ ‘ ∅ ) C 𝑁 ) )
5	2 3 4	sylancr	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( ∅ 𝐶 𝑁 ) ) = ( ( ♯ ‘ ∅ ) C 𝑁 ) )
6		hash0	⊢ ( ♯ ‘ ∅ ) = 0
7	6	oveq1i	⊢ ( ( ♯ ‘ ∅ ) C 𝑁 ) = ( 0 C 𝑁 )
8		bc0k	⊢ ( 𝑁 ∈ ℕ → ( 0 C 𝑁 ) = 0 )
9	7 8	eqtrid	⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ ∅ ) C 𝑁 ) = 0 )
10	5 9	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( ∅ 𝐶 𝑁 ) ) = 0 )
11		ovex	⊢ ( ∅ 𝐶 𝑁 ) ∈ V
12		hasheq0	⊢ ( ( ∅ 𝐶 𝑁 ) ∈ V → ( ( ♯ ‘ ( ∅ 𝐶 𝑁 ) ) = 0 ↔ ( ∅ 𝐶 𝑁 ) = ∅ ) )
13	11 12	ax-mp	⊢ ( ( ♯ ‘ ( ∅ 𝐶 𝑁 ) ) = 0 ↔ ( ∅ 𝐶 𝑁 ) = ∅ )
14	10 13	sylib	⊢ ( 𝑁 ∈ ℕ → ( ∅ 𝐶 𝑁 ) = ∅ )