This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snfi

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002) (Proof shortened by BTernaryTau, 13-Jan-2025)

Ref Expression
Assertion snfi { 𝐴 } ∈ Fin

Proof

Step Hyp Ref Expression
1 1onn ⊢ 1o ∈ ω
2 ensn1g ⊢ ( 𝐴 ∈ V → { 𝐴 } ≈ 1o )
3 breq2 ⊢ ( 𝑥 = 1o → ( { 𝐴 } ≈ 𝑥 ↔ { 𝐴 } ≈ 1o ) )
4 3 rspcev ⊢ ( ( 1o ∈ ω ∧ { 𝐴 } ≈ 1o ) → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
5 1 2 4 sylancr ⊢ ( 𝐴 ∈ V → ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
6 isfi ⊢ ( { 𝐴 } ∈ Fin ↔ ∃ 𝑥 ∈ ω { 𝐴 } ≈ 𝑥 )
7 5 6 sylibr ⊢ ( 𝐴 ∈ V → { 𝐴 } ∈ Fin )
8 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
9 0fi ⊢ ∅ ∈ Fin
10 eleq1 ⊢ ( { 𝐴 } = ∅ → ( { 𝐴 } ∈ Fin ↔ ∅ ∈ Fin ) )
11 9 10 mpbiri ⊢ ( { 𝐴 } = ∅ → { 𝐴 } ∈ Fin )
12 8 11 sylbi ⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } ∈ Fin )
13 7 12 pm2.61i ⊢ { 𝐴 } ∈ Fin