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 )