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 | |- _om e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvex | |- ( ZZ>= ` 0 ) e. _V |
|
| 2 | 0z | |- 0 e. ZZ |
|
| 3 | eqid | |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) |
|
| 4 | 2 3 | om2uzf1oi | |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> ( ZZ>= ` 0 ) |
| 5 | f1ovv | |- ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> ( ZZ>= ` 0 ) -> ( _om e. _V <-> ( ZZ>= ` 0 ) e. _V ) ) |
|
| 6 | 4 5 | ax-mp | |- ( _om e. _V <-> ( ZZ>= ` 0 ) e. _V ) |
| 7 | 1 6 | mpbir | |- _om e. _V |