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	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to A\ne \varnothing$$
2		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
3	2	a1i	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{Rel}\preccurlyeq$$
4		brrelex1	$$⊢\left(\mathrm{Rel}\preccurlyeq \wedge A\preccurlyeq \mathrm{\omega }\right)\to A\in \mathrm{V}$$
5	3 4	mpancom	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$
6		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
7	5 6	syl	$$⊢A\preccurlyeq \mathrm{\omega }\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
8	7	adantr	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
9	1 8	mpbird	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \varnothing \prec A$$
10		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
11	10	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
12	11	a1i	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{\omega }\approx \mathbb{N}$$
13		domentr	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\approx \mathbb{N}\right)\to A\preccurlyeq \mathbb{N}$$
14	12 13	mpdan	$$⊢A\preccurlyeq \mathrm{\omega }\to A\preccurlyeq \mathbb{N}$$
15	14	adantr	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to A\preccurlyeq \mathbb{N}$$
16		fodomr	$$⊢\left(\varnothing \prec A\wedge A\preccurlyeq \mathbb{N}\right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}A$$
17	9 15 16	syl2anc	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge A\ne \varnothing \right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}A$$