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