Metamath Proof Explorer

Theorem snct

Description: A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016)

Ref Expression
Assertion snct 
|- ( A e. V -> { A } ~<_ _om )

Proof

Step Hyp Ref Expression
1 ensn1g 
 |-  ( A e. V -> { A } ~~ 1o )
2 peano1 
 |-  (/) e. _om
3 2 ne0ii 
 |-  _om =/= (/)
4 omex 
 |-  _om e. _V
5 4 0sdom 
 |-  ( (/) ~< _om <-> _om =/= (/) )
6 3 5 mpbir 
 |-  (/) ~< _om
7 0sdom1dom 
 |-  ( (/) ~< _om <-> 1o ~<_ _om )
8 6 7 mpbi 
 |-  1o ~<_ _om
9 endomtr 
 |-  ( ( { A } ~~ 1o /\ 1o ~<_ _om ) -> { A } ~<_ _om )
10 1 8 9 sylancl 
 |-  ( A e. V -> { A } ~<_ _om )