This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝐴 )