Metamath Proof Explorer

Theorem n0scut

Description: A cut form for surreal naturals. (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 0slt1s 
 |-  0s
28 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
29 22 28 ax-mp 
 |-  ( 0s +s 1s ) = 1s
30 27 29 breqtrri 
 |-  0s
31 22 a1i 
 |-  ( T. -> 1s e. No )
32 26 31 26 sltsubaddd 
 |-  ( T. -> ( ( 0s -s 1s )  0s
33 30 32 mpbiri 
 |-  ( T. -> ( 0s -s 1s )
34 25 26 33 ssltsn 
 |-  ( T. -> { ( 0s -s 1s ) } <
35 21 elexi 
 |-  0s e. _V
36 35 snelpw 
 |-  ( 0s e. No <-> { 0s } e. ~P No )
37 21 36 mpbi 
 |-  { 0s } e. ~P No
38 nulssgt 
 |-  ( { 0s } e. ~P No -> { 0s } <
39 37 38 ax-mp 
 |-  { 0s } <
40 39 a1i 
 |-  ( T. -> { 0s } <
41 34 40 cuteq0 
 |-  ( T. -> ( { ( 0s -s 1s ) } |s (/) ) = 0s )
42 41 mptru 
 |-  ( { ( 0s -s 1s ) } |s (/) ) = 0s
43 42 eqcomi 
 |-  0s = ( { ( 0s -s 1s ) } |s (/) )
44 ovex 
 |-  ( x -s 1s ) e. _V
45 oveq1 
 |-  ( b = ( x -s 1s ) -> ( b +s 1s ) = ( ( x -s 1s ) +s 1s ) )
46 45 eqeq2d 
 |-  ( b = ( x -s 1s ) -> ( a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) ) )
47 44 46 rexsn 
 |-  ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) )
48 n0sno 
 |-  ( x e. NN0_s -> x e. No )
49 npcans 
 |-  ( ( x e. No /\ 1s e. No ) -> ( ( x -s 1s ) +s 1s ) = x )
50 48 22 49 sylancl 
 |-  ( x e. NN0_s -> ( ( x -s 1s ) +s 1s ) = x )
51 50 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x -s 1s ) +s 1s ) = x )
52 51 eqeq2d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( ( x -s 1s ) +s 1s ) <-> a = x ) )
53 47 52 bitrid 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) )
54 53 alrimiv 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) )
55 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 ) )
56 54 55 sylibr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } )
57 oveq2 
 |-  ( b = 0s -> ( x +s b ) = ( x +s 0s ) )
58 57 eqeq2d 
 |-  ( b = 0s -> ( a = ( x +s b ) <-> a = ( x +s 0s ) ) )
59 35 58 rexsn 
 |-  ( E. b e. { 0s } a = ( x +s b ) <-> a = ( x +s 0s ) )
60 48 addsridd 
 |-  ( x e. NN0_s -> ( x +s 0s ) = x )
61 60 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 0s ) = x )
62 61 eqeq2d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( x +s 0s ) <-> a = x ) )
63 59 62 bitrid 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) )
64 63 alrimiv 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) )
65 absn 
 |-  ( { a | E. b e. { 0s } a = ( x +s b ) } = { x } <-> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) )
66 64 65 sylibr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { 0s } a = ( x +s b ) } = { x } )
67 56 66 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 } ) )
68 unidm 
 |-  ( { x } u. { x } ) = { x }
69 67 68 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 } )
70 rex0 
 |-  -. E. b e. (/) a = ( b +s 1s )
71 70 abf 
 |-  { a | E. b e. (/) a = ( b +s 1s ) } = (/)
72 rex0 
 |-  -. E. b e. (/) a = ( x +s b )
73 72 abf 
 |-  { a | E. b e. (/) a = ( x +s b ) } = (/)
74 71 73 uneq12i 
 |-  ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = ( (/) u. (/) )
75 un0 
 |-  ( (/) u. (/) ) = (/)
76 74 75 eqtri 
 |-  ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/)
77 76 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 ) } ) = (/) )
78 69 77 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 (/) ) )
79 subscl 
 |-  ( ( x e. No /\ 1s e. No ) -> ( x -s 1s ) e. No )
80 48 22 79 sylancl 
 |-  ( x e. NN0_s -> ( x -s 1s ) e. No )
81 80 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x -s 1s ) e. No )
82 44 snelpw 
 |-  ( ( x -s 1s ) e. No <-> { ( x -s 1s ) } e. ~P No )
83 81 82 sylib 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } e. ~P No )
84 nulssgt 
 |-  ( { ( x -s 1s ) } e. ~P No -> { ( x -s 1s ) } <
85 83 84 syl 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } <
86 39 a1i 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { 0s } <
87 simpr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x = ( { ( x -s 1s ) } |s (/) ) )
88 df-1s 
 |-  1s = ( { 0s } |s (/) )
89 88 a1i 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> 1s = ( { 0s } |s (/) ) )
90 85 86 87 89 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 ) } ) ) )
91 48 adantr 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x e. No )
92 pncans 
 |-  ( ( x e. No /\ 1s e. No ) -> ( ( x +s 1s ) -s 1s ) = x )
93 91 22 92 sylancl 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x +s 1s ) -s 1s ) = x )
94 93 sneqd 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( ( x +s 1s ) -s 1s ) } = { x } )
95 94 oveq1d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) = ( { x } |s (/) ) )
96 78 90 95 3eqtr4d 
 |-  ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) )
97 96 ex 
 |-  ( x e. NN0_s -> ( x = ( { ( x -s 1s ) } |s (/) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) )
98 5 10 15 20 43 97 n0sind 
 |-  ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) )