Description: The set of all non-negative surreal integers exists. This theorem avoids the axiom of infinity by including it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | n0sexg | |- ( _om e. _V -> NN0_s e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-n0s | |- NN0_s = ( rec ( ( f e. _V |-> ( f +s 1s ) ) , 0s ) " _om ) |
|
| 2 | rdgfun | |- Fun rec ( ( f e. _V |-> ( f +s 1s ) ) , 0s ) |
|
| 3 | funimaexg | |- ( ( Fun rec ( ( f e. _V |-> ( f +s 1s ) ) , 0s ) /\ _om e. _V ) -> ( rec ( ( f e. _V |-> ( f +s 1s ) ) , 0s ) " _om ) e. _V ) |
|
| 4 | 2 3 | mpan | |- ( _om e. _V -> ( rec ( ( f e. _V |-> ( f +s 1s ) ) , 0s ) " _om ) e. _V ) |
| 5 | 1 4 | eqeltrid | |- ( _om e. _V -> NN0_s e. _V ) |