hfsnOLD

Description: Obsolete version of hfsn as of 17-Sep-2026. (Contributed by Scott Fenton, 15-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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

Theorem hfsnOLD

Proof