This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnfoctb

Description: There exists a mapping from NN onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion nnfoctb 
|- ( ( A ~<_ _om /\ A =/= (/) ) -> E. f f : NN -onto-> A )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> A =/= (/) )
2 reldom 
 |-  Rel ~<_
3 2 a1i 
 |-  ( A ~<_ _om -> Rel ~<_ )
4 brrelex1 
 |-  ( ( Rel ~<_ /\ A ~<_ _om ) -> A e. _V )
5 3 4 mpancom 
 |-  ( A ~<_ _om -> A e. _V )
6 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
7 5 6 syl 
 |-  ( A ~<_ _om -> ( (/) ~< A <-> A =/= (/) ) )
8 7 adantr 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> ( (/) ~< A <-> A =/= (/) ) )
9 1 8 mpbird 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> (/) ~< A )
10 nnenom 
 |-  NN ~~ _om
11 10 ensymi 
 |-  _om ~~ NN
12 11 a1i 
 |-  ( A ~<_ _om -> _om ~~ NN )
13 domentr 
 |-  ( ( A ~<_ _om /\ _om ~~ NN ) -> A ~<_ NN )
14 12 13 mpdan 
 |-  ( A ~<_ _om -> A ~<_ NN )
15 14 adantr 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> A ~<_ NN )
16 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A )
17 9 15 16 syl2anc 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> E. f f : NN -onto-> A )