Metamath Proof Explorer

Theorem 0hf

Description: The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015)

Ref Expression
Assertion 0hf ⊢ ∅ ∈ Hf

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 peano2 ⊢ ∅ ∈ ω → suc ⁡ ∅ ∈ ω
3 1 2 ax-mp ⊢ suc ⁡ ∅ ∈ ω
4 0elpw ⊢ ∅ ∈ 𝒫 R1 ⁡ ∅
5 0elon ⊢ ∅ ∈ On
6 r1suc ⊢ ∅ ∈ On → R1 ⁡ suc ⁡ ∅ = 𝒫 R1 ⁡ ∅
7 5 6 ax-mp ⊢ R1 ⁡ suc ⁡ ∅ = 𝒫 R1 ⁡ ∅
8 4 7 eleqtrri ⊢ ∅ ∈ R1 ⁡ suc ⁡ ∅
9 fveq2 ⊢ x = suc ⁡ ∅ → R1 ⁡ x = R1 ⁡ suc ⁡ ∅
10 9 eleq2d ⊢ x = suc ⁡ ∅ → ∅ ∈ R1 ⁡ x ↔ ∅ ∈ R1 ⁡ suc ⁡ ∅
11 10 rspcev ⊢ suc ⁡ ∅ ∈ ω ∧ ∅ ∈ R1 ⁡ suc ⁡ ∅ → ∃ x ∈ ω ∅ ∈ R1 ⁡ x
12 3 8 11 mp2an ⊢ ∃ x ∈ ω ∅ ∈ R1 ⁡ x
13 elhf ⊢ ∅ ∈ Hf ↔ ∃ x ∈ ω ∅ ∈ R1 ⁡ x
14 12 13 mpbir ⊢ ∅ ∈ Hf