Theorem 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	⊢ ( 𝐴 ∈ 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 )