0hf

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

		Ref	Expression
	Assertion	0hf	$⊢ \emptyset \in Hf$

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2		peano2	$⊢ \emptyset \in ω \to suc \emptyset \in ω$
3	1 2	ax-mp	$⊢ suc \emptyset \in ω$
4		0elpw	$⊢ \emptyset \in 𝒫 R_{1} (\emptyset)$
5		0elon	$⊢ \emptyset \in On$
6		r1suc	$⊢ \emptyset \in On \to R_{1} (suc \emptyset) = 𝒫 R_{1} (\emptyset)$
7	5 6	ax-mp	$⊢ R_{1} (suc \emptyset) = 𝒫 R_{1} (\emptyset)$
8	4 7	eleqtrri	$⊢ \emptyset \in R_{1} (suc \emptyset)$
9		fveq2	$⊢ x = suc \emptyset \to R_{1} (x) = R_{1} (suc \emptyset)$
10	9	eleq2d	$⊢ x = suc \emptyset \to (\emptyset \in R_{1} (x) \leftrightarrow \emptyset \in R_{1} (suc \emptyset))$
11	10	rspcev	$⊢ (suc \emptyset \in ω \land \emptyset \in R_{1} (suc \emptyset)) \to \exists x \in ω \emptyset \in R_{1} (x)$
12	3 8 11	mp2an	$⊢ \exists x \in ω \emptyset \in R_{1} (x)$
13		elhf	$⊢ \emptyset \in Hf \leftrightarrow \exists x \in ω \emptyset \in R_{1} (x)$
14	12 13	mpbir	$⊢ \emptyset \in Hf$

Metamath Proof Explorer