Metamath Proof Explorer

Theorem n0scut

Description: A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025)

Ref Expression
Assertion n0scut 
|- ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( y = 0s -> y = 0s )
2 oveq1 
 |-  ( y = 0s -> ( y -s 1s ) = ( 0s -s 1s ) )
3 2 sneqd 
 |-  ( y = 0s -> { ( y -s 1s ) } = { ( 0s -s 1s ) } )
4 3 oveq1d 
 |-  ( y = 0s -> ( { ( y -s 1s ) } |s (/) ) = ( { ( 0s -s 1s ) } |s (/) ) )
5 1 4 eqeq12d 
 |-  ( y = 0s -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> 0s = ( { ( 0s -s 1s ) } |s (/) ) ) )
6 id 
 |-  ( y = x -> y = x )
7 oveq1 
 |-  ( y = x -> ( y -s 1s ) = ( x -s 1s ) )
8 7 sneqd 
 |-  ( y = x -> { ( y -s 1s ) } = { ( x -s 1s ) } )
9 8 oveq1d 
 |-  ( y = x -> ( { ( y -s 1s ) } |s (/) ) = ( { ( x -s 1s ) } |s (/) ) )
10 6 9 eqeq12d 
 |-  ( y = x -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> x = ( { ( x -s 1s ) } |s (/) ) ) )
11 id 
 |-  ( y = ( x +s 1s ) -> y = ( x +s 1s ) )
12 oveq1 
 |-  ( y = ( x +s 1s ) -> ( y -s 1s ) = ( ( x +s 1s ) -s 1s ) )
13 12 sneqd 
 |-  ( y = ( x +s 1s ) -> { ( y -s 1s ) } = { ( ( x +s 1s ) -s 1s ) } )
14 13 oveq1d 
 |-  ( y = ( x +s 1s ) -> ( { ( y -s 1s ) } |s (/) ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) )
15 11 14 eqeq12d 
 |-  ( y = ( x +s 1s ) -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) )
16 id 
 |-  ( y = A -> y = A )
17 oveq1 
 |-  ( y = A -> ( y -s 1s ) = ( A -s 1s ) )
18 17 sneqd 
 |-  ( y = A -> { ( y -s 1s ) } = { ( A -s 1s ) } )
19 18 oveq1d 
 |-  ( y = A -> ( { ( y -s 1s ) } |s (/) ) = ( { ( A -s 1s ) } |s (/) ) )
20 16 19 eqeq12d 
 |-  ( y = A -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> A = ( { ( A -s 1s ) } |s (/) ) ) )
21 0sno 
 |-  0s e. No
22 1sno 
 |-  1s e. No
23 subscl 
 |-  ( ( 0s e. No /\ 1s e. No ) -> ( 0s -s 1s ) e. No )
24 21 22 23 mp2an 
 |-  ( 0s -s 1s ) e. No
25 24 a1i 
 |-  ( T. -> ( 0s -s 1s ) e. No )
26 21 a1i 
 |-  ( T. -> 0s e. No )
27 26 sltm1d 
 |-  ( T. -> ( 0s -s 1s )
28 25 27 cutneg 
 |-  ( T. -> ( { ( 0s -s 1s ) } |s (/) ) = 0s )
29 28 mptru 
 |-  ( { ( 0s -s 1s ) } |s (/) ) = 0s
30 29 eqcomi 
 |-  0s = ( { ( 0s -s 1s ) } |s (/) )
31 ovex 
 |-  ( x -s 1s ) e. _V
32 oveq1 
 |-  ( b = ( x -s 1s ) -> ( b +s 1s ) = ( ( x -s 1s ) +s 1s ) )
33 32 eqeq2d 
 |-  ( b = ( x -s 1s ) -> ( a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) ) )
34 31 33 rexsn 
 |-  ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) )
35 n0sno 
 |-  ( x e. NN0_s -> x e. No )
36 npcans 
 |-  ( ( x e. No /\ 1s e. No ) -> ( ( x -s 1s ) +s 1s ) = x )
37 35 22 36 sylancl 
 |-  ( x e. NN0_s -> ( ( x -s 1s ) +s 1s ) = x )
38 37 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x -s 1s ) +s 1s ) = x )
39 38 eqeq2d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( ( x -s 1s ) +s 1s ) <-> a = x ) )
40 34 39 bitrid 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) )
41 40 alrimiv 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) )
42 absn 
 |-  ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } <-> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) )
43 41 42 sylibr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } )
44 21 elexi 
 |-  0s e. _V
45 oveq2 
 |-  ( b = 0s -> ( x +s b ) = ( x +s 0s ) )
46 45 eqeq2d 
 |-  ( b = 0s -> ( a = ( x +s b ) <-> a = ( x +s 0s ) ) )
47 44 46 rexsn 
 |-  ( E. b e. { 0s } a = ( x +s b ) <-> a = ( x +s 0s ) )
48 35 addsridd 
 |-  ( x e. NN0_s -> ( x +s 0s ) = x )
49 48 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 0s ) = x )
50 49 eqeq2d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( x +s 0s ) <-> a = x ) )
51 47 50 bitrid 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) )
52 51 alrimiv 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) )
53 absn 
 |-  ( { a | E. b e. { 0s } a = ( x +s b ) } = { x } <-> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) )
54 52 53 sylibr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { 0s } a = ( x +s b ) } = { x } )
55 43 54 uneq12d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) = ( { x } u. { x } ) )
56 unidm 
 |-  ( { x } u. { x } ) = { x }
57 55 56 eqtrdi 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) = { x } )
58 rex0 
 |-  -. E. b e. (/) a = ( b +s 1s )
59 58 abf 
 |-  { a | E. b e. (/) a = ( b +s 1s ) } = (/)
60 rex0 
 |-  -. E. b e. (/) a = ( x +s b )
61 60 abf 
 |-  { a | E. b e. (/) a = ( x +s b ) } = (/)
62 59 61 uneq12i 
 |-  ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = ( (/) u. (/) )
63 un0 
 |-  ( (/) u. (/) ) = (/)
64 62 63 eqtri 
 |-  ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/)
65 64 a1i 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/) )
66 57 65 oveq12d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) |s ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) ) = ( { x } |s (/) ) )
67 subscl 
 |-  ( ( x e. No /\ 1s e. No ) -> ( x -s 1s ) e. No )
68 35 22 67 sylancl 
 |-  ( x e. NN0_s -> ( x -s 1s ) e. No )
69 68 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x -s 1s ) e. No )
70 31 snelpw 
 |-  ( ( x -s 1s ) e. No <-> { ( x -s 1s ) } e. ~P No )
71 69 70 sylib 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } e. ~P No )
72 nulssgt 
 |-  ( { ( x -s 1s ) } e. ~P No -> { ( x -s 1s ) } <
73 71 72 syl 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } <
74 44 snelpw 
 |-  ( 0s e. No <-> { 0s } e. ~P No )
75 21 74 mpbi 
 |-  { 0s } e. ~P No
76 nulssgt 
 |-  ( { 0s } e. ~P No -> { 0s } <
77 75 76 mp1i 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { 0s } <
78 simpr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x = ( { ( x -s 1s ) } |s (/) ) )
79 df-1s 
 |-  1s = ( { 0s } |s (/) )
80 79 a1i 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> 1s = ( { 0s } |s (/) ) )
81 73 77 78 80 addsunif 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) |s ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) ) )
82 35 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x e. No )
83 pncans 
 |-  ( ( x e. No /\ 1s e. No ) -> ( ( x +s 1s ) -s 1s ) = x )
84 82 22 83 sylancl 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x +s 1s ) -s 1s ) = x )
85 84 sneqd 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( ( x +s 1s ) -s 1s ) } = { x } )
86 85 oveq1d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) = ( { x } |s (/) ) )
87 66 81 86 3eqtr4d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) )
88 87 ex 
 |-  ( x e. NN0_s -> ( x = ( { ( x -s 1s ) } |s (/) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) )
89 5 10 15 20 30 88 n0sind 
 |-  ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) )