Theorem 0hf

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

	Ref	Expression
Assertion	0hf	Could not format assertion : No typesetting found for |- (/) e. HF with typecode |-

Proof

Step	Hyp	Ref	Expression
1		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
2		peano2	$$⊢\varnothing \in \mathrm{\omega }\to \mathrm{suc}\varnothing \in \mathrm{\omega }$$
3	1 2	ax-mp	$$⊢\mathrm{suc}\varnothing \in \mathrm{\omega }$$
4		0elpw	$$⊢\varnothing \in 𝒫R_1\left(\varnothing \right)$$
5		0elon	$$⊢\varnothing \in \mathrm{On}$$
6		r1suc	$$⊢\varnothing \in \mathrm{On}\to R_1\left(\mathrm{suc}\varnothing \right)=𝒫R_1\left(\varnothing \right)$$
7	5 6	ax-mp	$$⊢R_1\left(\mathrm{suc}\varnothing \right)=𝒫R_1\left(\varnothing \right)$$
8	4 7	eleqtrri	$$⊢\varnothing \in R_1\left(\mathrm{suc}\varnothing \right)$$
9		fveq2	$$⊢x=\mathrm{suc}\varnothing \to R_1\left(x\right)=R_1\left(\mathrm{suc}\varnothing \right)$$
10	9	eleq2d	$$⊢x=\mathrm{suc}\varnothing \to \left(\varnothing \in R_1\left(x\right)\leftrightarrow \varnothing \in R_1\left(\mathrm{suc}\varnothing \right)\right)$$
11	10	rspcev	$$⊢\left(\mathrm{suc}\varnothing \in \mathrm{\omega }\wedge \varnothing \in R_1\left(\mathrm{suc}\varnothing \right)\right)\to \exists x\in \mathrm{\omega }\varnothing \in R_1\left(x\right)$$
12	3 8 11	mp2an	$$⊢\exists x\in \mathrm{\omega }\varnothing \in R_1\left(x\right)$$
13		elhf	Could not format ( (/) e. HF <-> E. x e. _om (/) e. ( R1 ` x ) ) : No typesetting found for |- ( (/) e. HF <-> E. x e. _om (/) e. ( R1 ` x ) ) with typecode |-
14	12 13	mpbir	Could not format (/) e. HF : No typesetting found for |- (/) e. HF with typecode |-