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 ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
4	2 3	om2uzf1oi	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ( ℤ≥ ‘ 0 )
5		f1ovv	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ( ℤ≥ ‘ 0 ) → ( ω ∈ V ↔ ( ℤ≥ ‘ 0 ) ∈ V ) )
6	4 5	ax-mp	⊢ ( ω ∈ V ↔ ( ℤ≥ ‘ 0 ) ∈ V )
7	1 6	mpbir	⊢ ω ∈ V