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 
|- NN0_s = |^| { x | ( 0s e. x /\ A. y e. x ( y +s 1s ) e. x ) }

Proof

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