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 ∅ ∈ 𝒫 ( 𝑅1 ‘ ∅ )
5 0elon ∅ ∈ On
6 r1suc ( ∅ ∈ On → ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ ) )
7 5 6 ax-mp ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ )
8 4 7 eleqtrri ∅ ∈ ( 𝑅1 ‘ suc ∅ )
9 fveq2 ( 𝑥 = suc ∅ → ( 𝑅1𝑥 ) = ( 𝑅1 ‘ suc ∅ ) )
10 9 eleq2d ( 𝑥 = suc ∅ → ( ∅ ∈ ( 𝑅1𝑥 ) ↔ ∅ ∈ ( 𝑅1 ‘ suc ∅ ) ) )
11 10 rspcev ( ( suc ∅ ∈ ω ∧ ∅ ∈ ( 𝑅1 ‘ suc ∅ ) ) → ∃ 𝑥 ∈ ω ∅ ∈ ( 𝑅1𝑥 ) )
12 3 8 11 mp2an 𝑥 ∈ ω ∅ ∈ ( 𝑅1𝑥 )
13 elhf ( ∅ ∈ Hf ↔ ∃ 𝑥 ∈ ω ∅ ∈ ( 𝑅1𝑥 ) )
14 12 13 mpbir ∅ ∈ Hf