# Metamath Proof Explorer

## Theorem snfi

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002)

Ref Expression
Assertion snfi ${⊢}\left\{{A}\right\}\in \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 1onn ${⊢}{1}_{𝑜}\in \mathrm{\omega }$
2 ensn1g ${⊢}{A}\in \mathrm{V}\to \left\{{A}\right\}\approx {1}_{𝑜}$
3 breq2 ${⊢}{x}={1}_{𝑜}\to \left(\left\{{A}\right\}\approx {x}↔\left\{{A}\right\}\approx {1}_{𝑜}\right)$
4 3 rspcev ${⊢}\left({1}_{𝑜}\in \mathrm{\omega }\wedge \left\{{A}\right\}\approx {1}_{𝑜}\right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
5 1 2 4 sylancr ${⊢}{A}\in \mathrm{V}\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
6 snprc ${⊢}¬{A}\in \mathrm{V}↔\left\{{A}\right\}=\varnothing$
7 en0 ${⊢}\left\{{A}\right\}\approx \varnothing ↔\left\{{A}\right\}=\varnothing$
8 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
9 breq2 ${⊢}{x}=\varnothing \to \left(\left\{{A}\right\}\approx {x}↔\left\{{A}\right\}\approx \varnothing \right)$
10 9 rspcev ${⊢}\left(\varnothing \in \mathrm{\omega }\wedge \left\{{A}\right\}\approx \varnothing \right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
11 8 10 mpan ${⊢}\left\{{A}\right\}\approx \varnothing \to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
12 7 11 sylbir ${⊢}\left\{{A}\right\}=\varnothing \to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
13 6 12 sylbi ${⊢}¬{A}\in \mathrm{V}\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
14 5 13 pm2.61i ${⊢}\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
15 isfi ${⊢}\left\{{A}\right\}\in \mathrm{Fin}↔\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}\approx {x}$
16 14 15 mpbir ${⊢}\left\{{A}\right\}\in \mathrm{Fin}$