Theorem hfsn

Description: The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	hfsn	|- ( A e. Hf -> { A } e. Hf )

Proof

Step	Hyp	Ref	Expression
1		ranksng	|- ( A e. Hf -> ( rank ` { A } ) = suc ( rank ` A ) )
2		elhf2g	|- ( A e. Hf -> ( A e. Hf <-> ( rank ` A ) e. _om ) )
3	2	ibi	|- ( A e. Hf -> ( rank ` A ) e. _om )
4		peano2	|- ( ( rank ` A ) e. _om -> suc ( rank ` A ) e. _om )
5	3 4	syl	|- ( A e. Hf -> suc ( rank ` A ) e. _om )
6	1 5	eqeltrd	|- ( A e. Hf -> ( rank ` { A } ) e. _om )
7		snex	|- { A } e. _V
8	7	elhf2	|- ( { A } e. Hf <-> ( rank ` { A } ) e. _om )
9	6 8	sylibr	|- ( A e. Hf -> { A } e. Hf )