Metamath Proof Explorer

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 ∈ Hf → A ∈ Hf

Proof

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