Theorem hfsn

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

	Ref	Expression
Assertion	hfsn	⊢ ( 𝐴 ∈ Hf → { 𝐴 } ∈ Hf )

Proof

Step	Hyp	Ref	Expression
1		ranksng	⊢ ( 𝐴 ∈ Hf → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )
2		elhf2g	⊢ ( 𝐴 ∈ Hf → ( 𝐴 ∈ Hf ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
3	2	ibi	⊢ ( 𝐴 ∈ Hf → ( rank ‘ 𝐴 ) ∈ ω )
4		peano2	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → suc ( rank ‘ 𝐴 ) ∈ ω )
5	3 4	syl	⊢ ( 𝐴 ∈ Hf → suc ( rank ‘ 𝐴 ) ∈ ω )
6	1 5	eqeltrd	⊢ ( 𝐴 ∈ Hf → ( rank ‘ { 𝐴 } ) ∈ ω )
7		snex	⊢ { 𝐴 } ∈ V
8	7	elhf2	⊢ ( { 𝐴 } ∈ Hf ↔ ( rank ‘ { 𝐴 } ) ∈ ω )
9	6 8	sylibr	⊢ ( 𝐴 ∈ Hf → { 𝐴 } ∈ Hf )