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 )