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 ≼ ω \land A \neq \emptyset) \to \exists f f : ℕ \underset{onto}{⟶} A$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A ≼ ω \land A \neq \emptyset) \to A \neq \emptyset$
2		reldom	$⊢ Rel ≼$
3	2	a1i	$⊢ A ≼ ω \to Rel ≼$
4		brrelex1	$⊢ (Rel ≼ \land A ≼ ω) \to A \in V$
5	3 4	mpancom	$⊢ A ≼ ω \to A \in V$
6		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
7	5 6	syl	$⊢ A ≼ ω \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
8	7	adantr	$⊢ (A ≼ ω \land A \neq \emptyset) \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
9	1 8	mpbird	$⊢ (A ≼ ω \land A \neq \emptyset) \to \emptyset ≺ A$
10		nnenom	$⊢ ℕ \approx ω$
11	10	ensymi	$⊢ ω \approx ℕ$
12	11	a1i	$⊢ A ≼ ω \to ω \approx ℕ$
13		domentr	$⊢ (A ≼ ω \land ω \approx ℕ) \to A ≼ ℕ$
14	12 13	mpdan	$⊢ A ≼ ω \to A ≼ ℕ$
15	14	adantr	$⊢ (A ≼ ω \land A \neq \emptyset) \to A ≼ ℕ$
16		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} A$
17	9 15 16	syl2anc	$⊢ (A ≼ ω \land A \neq \emptyset) \to \exists f f : ℕ \underset{onto}{⟶} A$

Metamath Proof Explorer