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	⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
2		reldom	⊢ Rel ≼
3	2	a1i	⊢ ( 𝐴 ≼ ω → Rel ≼ )
4		brrelex1	⊢ ( ( Rel ≼ ∧ 𝐴 ≼ ω ) → 𝐴 ∈ V )
5	3 4	mpancom	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
6		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7	5 6	syl	⊢ ( 𝐴 ≼ ω → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
8	7	adantr	⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
9	1 8	mpbird	⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∅ ≺ 𝐴 )
10		nnenom	⊢ ℕ ≈ ω
11	10	ensymi	⊢ ω ≈ ℕ
12	11	a1i	⊢ ( 𝐴 ≼ ω → ω ≈ ℕ )
13		domentr	⊢ ( ( 𝐴 ≼ ω ∧ ω ≈ ℕ ) → 𝐴 ≼ ℕ )
14	12 13	mpdan	⊢ ( 𝐴 ≼ ω → 𝐴 ≼ ℕ )
15	14	adantr	⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → 𝐴 ≼ ℕ )
16		fodomr	⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )
17	9 15 16	syl2anc	⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )