hfsn

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

		Ref	Expression
	Assertion	hfsn	$⊢ A \in Hf \to \{A\} \in Hf$

Step	Hyp	Ref	Expression
1		ranksng	$⊢ A \in Hf \to rank (\{A\}) = suc rank (A)$
2		elhf2g	$⊢ A \in Hf \to (A \in Hf \leftrightarrow rank (A) \in ω)$
3	2	ibi	$⊢ A \in Hf \to rank (A) \in ω$
4		peano2	$⊢ rank (A) \in ω \to suc rank (A) \in ω$
5	3 4	syl	$⊢ A \in Hf \to suc rank (A) \in ω$
6	1 5	eqeltrd	$⊢ A \in Hf \to rank (\{A\}) \in ω$
7		snex	$⊢ \{A\} \in V$
8	7	elhf2	$⊢ \{A\} \in Hf \leftrightarrow rank (\{A\}) \in ω$
9	6 8	sylibr	$⊢ A \in Hf \to \{A\} \in Hf$

Metamath Proof Explorer