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