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