Metamath Proof Explorer


Theorem unbnn3

Description: Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005)

Ref Expression
Assertion unbnn3 ( ( 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦𝐴 𝑥𝑦 ) → 𝐴 ≈ ω )

Proof

Step Hyp Ref Expression
1 omex ω ∈ V
2 unbnn ( ( ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦𝐴 𝑥𝑦 ) → 𝐴 ≈ ω )
3 1 2 mp3an1 ( ( 𝐴 ⊆ ω ∧ ∀ 𝑥 ∈ ω ∃ 𝑦𝐴 𝑥𝑦 ) → 𝐴 ≈ ω )