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 
|- { A } e. Fin

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 ensn1g 
 |-  ( A e. _V -> { A } ~~ 1o )
3 breq2 
 |-  ( x = 1o -> ( { A } ~~ x <-> { A } ~~ 1o ) )
4 3 rspcev 
 |-  ( ( 1o e. _om /\ { A } ~~ 1o ) -> E. x e. _om { A } ~~ x )
5 1 2 4 sylancr 
 |-  ( A e. _V -> E. x e. _om { A } ~~ x )
6 isfi 
 |-  ( { A } e. Fin <-> E. x e. _om { A } ~~ x )
7 5 6 sylibr 
 |-  ( A e. _V -> { A } e. Fin )
8 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
9 0fi 
 |-  (/) e. Fin
10 eleq1 
 |-  ( { A } = (/) -> ( { A } e. Fin <-> (/) e. Fin ) )
11 9 10 mpbiri 
 |-  ( { A } = (/) -> { A } e. Fin )
12 8 11 sylbi 
 |-  ( -. A e. _V -> { A } e. Fin )
13 7 12 pm2.61i 
 |-  { A } e. Fin