Theorem elhf2g

Description: Hereditarily finiteness via rank. Closed form of elhf2 . (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	elhf2g	Could not format assertion : No typesetting found for |- ( A e. V -> ( A e. HF <-> ( rank ` A ) e. _om ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eleq1	Could not format ( x = A -> ( x e. HF <-> A e. HF ) ) : No typesetting found for |- ( x = A -> ( x e. HF <-> A e. HF ) ) with typecode |-
2		fveq2	$$⊢x=A\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(A\right)$$
3	2	eleq1d	$$⊢x=A\to \left(\mathrm{rank}\left(x\right)\in \mathrm{\omega }\leftrightarrow \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	elhf2	Could not format ( x e. HF <-> ( rank ` x ) e. _om ) : No typesetting found for |- ( x e. HF <-> ( rank ` x ) e. _om ) with typecode |-
6	1 3 5	vtoclbg	Could not format ( A e. V -> ( A e. HF <-> ( rank ` A ) e. _om ) ) : No typesetting found for |- ( A e. V -> ( A e. HF <-> ( rank ` A ) e. _om ) ) with typecode |-