Metamath Proof Explorer

Theorem omexcn

Description: The axioms of the complex numbers imply the Axiom of Infinity (in the form of omex ): the map of om2uzf1oi is a one-to-one onto mapping from _om onto a set of integers, so _om is a set. Compare dcomex and grothomex . Note that our proof depends on neither ax-inf nor ax-inf2 . (Contributed by Timothy J. O'Malley, 8-Oct-2026)

Ref Expression
Assertion omexcn ⊢ ω ∈ V

Proof

Step Hyp Ref Expression
1 fvex ⊢ ℤ ≥ 0 ∈ V
2 0z ⊢ 0 ∈ ℤ
3 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
4 2 3 om2uzf1oi ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω : ω ⟶ 1-1 onto ℤ ≥ 0
5 f1ovv ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω : ω ⟶ 1-1 onto ℤ ≥ 0 → ω ∈ V ↔ ℤ ≥ 0 ∈ V
6 4 5 ax-mp ⊢ ω ∈ V ↔ ℤ ≥ 0 ∈ V
7 1 6 mpbir ⊢ ω ∈ V