Metamath Proof Explorer

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 ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
Assertion 0hashbc ⊢ N ∈ ℕ → ∅ C N = ∅

Proof

Step Hyp Ref Expression
1 ramval.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 0fin ⊢ ∅ ∈ Fin
3 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
4 1 hashbc2 ⊢ ∅ ∈ Fin ∧ N ∈ ℕ 0 → ∅ C N = ( ∅ N)
5 2 3 4 sylancr ⊢ N ∈ ℕ → ∅ C N = ( ∅ N)
6 hash0 ⊢ ∅ = 0
7 6 oveq1i ⊢ ( ∅ N) = ( 0 N)
8 bc0k ⊢ N ∈ ℕ → ( 0 N) = 0
9 7 8 eqtrid ⊢ N ∈ ℕ → ( ∅ N) = 0
10 5 9 eqtrd ⊢ N ∈ ℕ → ∅ C N = 0
11 ovex ⊢ ∅ C N ∈ V
12 hasheq0 ⊢ ∅ C N ∈ V → ∅ C N = 0 ↔ ∅ C N = ∅
13 11 12 ax-mp ⊢ ∅ C N = 0 ↔ ∅ C N = ∅
14 10 13 sylib ⊢ N ∈ ℕ → ∅ C N = ∅