Metamath Proof Explorer

Theorem dfn0s2

Description: Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

Ref Expression
Assertion dfn0s2 Could not format assertion : No typesetting found for |- NN0_s = |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } with typecode |-

Proof

Step Hyp Ref Expression
1 0sno Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2 1 elexi Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
3 2 elintab Could not format ( 0s e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> 0s e. x ) ) : No typesetting found for |- ( 0s e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> 0s e. x ) ) with typecode |-
4 simpl Could not format ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> 0s e. x ) : No typesetting found for |- ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> 0s e. x ) with typecode |-
5 3 4 mpgbir Could not format 0s e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } : No typesetting found for |- 0s e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } with typecode |-
6 oveq1 Could not format ( y = z -> ( y +s 1s ) = ( z +s 1s ) ) : No typesetting found for |- ( y = z -> ( y +s 1s ) = ( z +s 1s ) ) with typecode |-
7 6 eleq1d Could not format ( y = z -> ( ( y +s 1s ) e. x <-> ( z +s 1s ) e. x ) ) : No typesetting found for |- ( y = z -> ( ( y +s 1s ) e. x <-> ( z +s 1s ) e. x ) ) with typecode |-
8 7 rspccv Could not format ( A. y e. x ( y +s 1s ) e. x -> ( z e. x -> ( z +s 1s ) e. x ) ) : No typesetting found for |- ( A. y e. x ( y +s 1s ) e. x -> ( z e. x -> ( z +s 1s ) e. x ) ) with typecode |-
9 8 adantl Could not format ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z e. x -> ( z +s 1s ) e. x ) ) : No typesetting found for |- ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z e. x -> ( z +s 1s ) e. x ) ) with typecode |-
10 9 a2i Could not format ( ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> z e. x ) -> ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z +s 1s ) e. x ) ) : No typesetting found for |- ( ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> z e. x ) -> ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z +s 1s ) e. x ) ) with typecode |-
11 10 alimi Could not format ( A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> z e. x ) -> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z +s 1s ) e. x ) ) : No typesetting found for |- ( A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> z e. x ) -> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z +s 1s ) e. x ) ) with typecode |-
12 vex ⊢z∈V
13 12 elintab Could not format ( z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> z e. x ) ) : No typesetting found for |- ( z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> z e. x ) ) with typecode |-
14 ovex Could not format ( z +s 1s ) e. _V : No typesetting found for |- ( z +s 1s ) e. _V with typecode |-
15 14 elintab Could not format ( ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z +s 1s ) e. x ) ) : No typesetting found for |- ( ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> A. x ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) -> ( z +s 1s ) e. x ) ) with typecode |-
16 11 13 15 3imtr4i Could not format ( z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } -> ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ) : No typesetting found for |- ( z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } -> ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ) with typecode |-
17 16 rgen Could not format A. z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } : No typesetting found for |- A. z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } with typecode |-
18 peano5n0s Could not format ( ( 0s e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } /\ A. z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ) -> NN0_s C_ |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ) : No typesetting found for |- ( ( 0s e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } /\ A. z e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ( z +s 1s ) e. |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ) -> NN0_s C_ |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } ) with typecode |-
19 5 17 18 mp2an Could not format NN0_s C_ |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } : No typesetting found for |- NN0_s C_ |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } with typecode |-
20 0n0s Could not format 0s e. NN0_s : No typesetting found for |- 0s e. NN0_s with typecode |-
21 peano2n0s Could not format ( y e. NN0_s -> ( y +s 1s ) e. NN0_s ) : No typesetting found for |- ( y e. NN0_s -> ( y +s 1s ) e. NN0_s ) with typecode |-
22 21 rgen Could not format A. y e. NN0_s ( y +s 1s ) e. NN0_s : No typesetting found for |- A. y e. NN0_s ( y +s 1s ) e. NN0_s with typecode |-
23 n0sex Could not format NN0_s e. _V : No typesetting found for |- NN0_s e. _V with typecode |-
24 eleq2 Could not format ( x = NN0_s -> ( 0s e. x <-> 0s e. NN0_s ) ) : No typesetting found for |- ( x = NN0_s -> ( 0s e. x <-> 0s e. NN0_s ) ) with typecode |-
25 eleq2 Could not format ( x = NN0_s -> ( ( y +s 1s ) e. x <-> ( y +s 1s ) e. NN0_s ) ) : No typesetting found for |- ( x = NN0_s -> ( ( y +s 1s ) e. x <-> ( y +s 1s ) e. NN0_s ) ) with typecode |-
26 25 raleqbi1dv Could not format ( x = NN0_s -> ( A. y e. x ( y +s 1s ) e. x <-> A. y e. NN0_s ( y +s 1s ) e. NN0_s ) ) : No typesetting found for |- ( x = NN0_s -> ( A. y e. x ( y +s 1s ) e. x <-> A. y e. NN0_s ( y +s 1s ) e. NN0_s ) ) with typecode |-
27 24 26 anbi12d Could not format ( x = NN0_s -> ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) <-> ( 0s e. NN0_s /\ A. y e. NN0_s ( y +s 1s ) e. NN0_s ) ) ) : No typesetting found for |- ( x = NN0_s -> ( ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) <-> ( 0s e. NN0_s /\ A. y e. NN0_s ( y +s 1s ) e. NN0_s ) ) ) with typecode |-
28 23 27 elab Could not format ( NN0_s e. { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> ( 0s e. NN0_s /\ A. y e. NN0_s ( y +s 1s ) e. NN0_s ) ) : No typesetting found for |- ( NN0_s e. { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } <-> ( 0s e. NN0_s /\ A. y e. NN0_s ( y +s 1s ) e. NN0_s ) ) with typecode |-
29 20 22 28 mpbir2an Could not format NN0_s e. { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } : No typesetting found for |- NN0_s e. { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } with typecode |-
30 intss1 Could not format ( NN0_s e. { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } -> |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } C_ NN0_s ) : No typesetting found for |- ( NN0_s e. { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } -> |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } C_ NN0_s ) with typecode |-
31 29 30 ax-mp Could not format |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } C_ NN0_s : No typesetting found for |- |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } C_ NN0_s with typecode |-
32 19 31 eqssi Could not format NN0_s = |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } : No typesetting found for |- NN0_s = |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) } with typecode |-