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 Fin

Proof

Step Hyp Ref Expression
1 1onn 1 𝑜 ω
2 ensn1g A V A 1 𝑜
3 breq2 x = 1 𝑜 A x A 1 𝑜
4 3 rspcev 1 𝑜 ω A 1 𝑜 x ω A x
5 1 2 4 sylancr A V x ω A x
6 isfi A Fin x ω A x
7 5 6 sylibr A V A Fin
8 snprc ¬ A V A =
9 0fi Fin
10 eleq1 A = A Fin Fin
11 9 10 mpbiri A = A Fin
12 8 11 sylbi ¬ A V A Fin
13 7 12 pm2.61i A Fin