Metamath Proof Explorer

Theorem recut

Description: The cut involved in defining surreal reals is a genuine cut. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion recut 
|- ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <

Proof

Step Hyp Ref Expression
1 nnsex 
 |-  NN_s e. _V
2 1 abrexex 
 |-  { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } e. _V
3 2 a1i 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } e. _V )
4 1 abrexex 
 |-  { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } e. _V
5 4 a1i 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } e. _V )
6 1sno 
 |-  1s e. No
7 6 a1i 
 |-  ( n e. NN_s -> 1s e. No )
8 nnsno 
 |-  ( n e. NN_s -> n e. No )
9 nnne0s 
 |-  ( n e. NN_s -> n =/= 0s )
10 7 8 9 divscld 
 |-  ( n e. NN_s -> ( 1s /su n ) e. No )
11 subscl 
 |-  ( ( A e. No /\ ( 1s /su n ) e. No ) -> ( A -s ( 1s /su n ) ) e. No )
12 10 11 sylan2 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No )
13 eleq1 
 |-  ( x = ( A -s ( 1s /su n ) ) -> ( x e. No <-> ( A -s ( 1s /su n ) ) e. No ) )
14 12 13 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( x = ( A -s ( 1s /su n ) ) -> x e. No ) )
15 14 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s x = ( A -s ( 1s /su n ) ) -> x e. No ) )
16 15 abssdv 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } C_ No )
17 addscl 
 |-  ( ( A e. No /\ ( 1s /su n ) e. No ) -> ( A +s ( 1s /su n ) ) e. No )
18 10 17 sylan2 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A +s ( 1s /su n ) ) e. No )
19 eleq1 
 |-  ( x = ( A +s ( 1s /su n ) ) -> ( x e. No <-> ( A +s ( 1s /su n ) ) e. No ) )
20 18 19 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( x = ( A +s ( 1s /su n ) ) -> x e. No ) )
21 20 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s x = ( A +s ( 1s /su n ) ) -> x e. No ) )
22 21 abssdv 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } C_ No )
23 vex 
 |-  y e. _V
24 eqeq1 
 |-  ( x = y -> ( x = ( A -s ( 1s /su n ) ) <-> y = ( A -s ( 1s /su n ) ) ) )
25 24 rexbidv 
 |-  ( x = y -> ( E. n e. NN_s x = ( A -s ( 1s /su n ) ) <-> E. n e. NN_s y = ( A -s ( 1s /su n ) ) ) )
26 23 25 elab 
 |-  ( y e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <-> E. n e. NN_s y = ( A -s ( 1s /su n ) ) )
27 vex 
 |-  z e. _V
28 eqeq1 
 |-  ( x = z -> ( x = ( A +s ( 1s /su n ) ) <-> z = ( A +s ( 1s /su n ) ) ) )
29 28 rexbidv 
 |-  ( x = z -> ( E. n e. NN_s x = ( A +s ( 1s /su n ) ) <-> E. n e. NN_s z = ( A +s ( 1s /su n ) ) ) )
30 oveq2 
 |-  ( n = m -> ( 1s /su n ) = ( 1s /su m ) )
31 30 oveq2d 
 |-  ( n = m -> ( A +s ( 1s /su n ) ) = ( A +s ( 1s /su m ) ) )
32 31 eqeq2d 
 |-  ( n = m -> ( z = ( A +s ( 1s /su n ) ) <-> z = ( A +s ( 1s /su m ) ) ) )
33 32 cbvrexvw 
 |-  ( E. n e. NN_s z = ( A +s ( 1s /su n ) ) <-> E. m e. NN_s z = ( A +s ( 1s /su m ) ) )
34 29 33 bitrdi 
 |-  ( x = z -> ( E. n e. NN_s x = ( A +s ( 1s /su n ) ) <-> E. m e. NN_s z = ( A +s ( 1s /su m ) ) ) )
35 27 34 elab 
 |-  ( z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } <-> E. m e. NN_s z = ( A +s ( 1s /su m ) ) )
36 26 35 anbi12i 
 |-  ( ( y e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } /\ z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) <-> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ E. m e. NN_s z = ( A +s ( 1s /su m ) ) ) )
37 reeanv 
 |-  ( E. n e. NN_s E. m e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ z = ( A +s ( 1s /su m ) ) ) <-> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ E. m e. NN_s z = ( A +s ( 1s /su m ) ) ) )
38 36 37 bitr4i 
 |-  ( ( y e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } /\ z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) <-> E. n e. NN_s E. m e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ z = ( A +s ( 1s /su m ) ) ) )
39 simpl 
 |-  ( ( A e. No /\ n e. NN_s ) -> A e. No )
40 10 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 1s /su n ) e. No )
41 39 40 subsvald 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) = ( A +s ( -us ` ( 1s /su n ) ) ) )
42 41 adantrr 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( A -s ( 1s /su n ) ) = ( A +s ( -us ` ( 1s /su n ) ) ) )
43 10 negscld 
 |-  ( n e. NN_s -> ( -us ` ( 1s /su n ) ) e. No )
44 43 adantr 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( -us ` ( 1s /su n ) ) e. No )
45 0sno 
 |-  0s e. No
46 45 a1i 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> 0s e. No )
47 6 a1i 
 |-  ( m e. NN_s -> 1s e. No )
48 nnsno 
 |-  ( m e. NN_s -> m e. No )
49 nnne0s 
 |-  ( m e. NN_s -> m =/= 0s )
50 47 48 49 divscld 
 |-  ( m e. NN_s -> ( 1s /su m ) e. No )
51 50 adantl 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( 1s /su m ) e. No )
52 id 
 |-  ( n e. NN_s -> n e. NN_s )
53 52 nnsrecgt0d 
 |-  ( n e. NN_s -> 0s
54 45 a1i 
 |-  ( n e. NN_s -> 0s e. No )
55 54 10 sltnegd 
 |-  ( n e. NN_s -> ( 0s  ( -us ` ( 1s /su n ) )
56 53 55 mpbid 
 |-  ( n e. NN_s -> ( -us ` ( 1s /su n ) )
57 negs0s 
 |-  ( -us ` 0s ) = 0s
58 56 57 breqtrdi 
 |-  ( n e. NN_s -> ( -us ` ( 1s /su n ) )
59 58 adantr 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( -us ` ( 1s /su n ) )
60 id 
 |-  ( m e. NN_s -> m e. NN_s )
61 60 nnsrecgt0d 
 |-  ( m e. NN_s -> 0s
62 61 adantl 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> 0s
63 44 46 51 59 62 slttrd 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( -us ` ( 1s /su n ) )
64 63 adantl 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( -us ` ( 1s /su n ) )
65 44 adantl 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( -us ` ( 1s /su n ) ) e. No )
66 50 ad2antll 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( 1s /su m ) e. No )
67 simpl 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> A e. No )
68 65 66 67 sltadd2d 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( ( -us ` ( 1s /su n ) )  ( A +s ( -us ` ( 1s /su n ) ) )
69 64 68 mpbid 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( A +s ( -us ` ( 1s /su n ) ) )
70 42 69 eqbrtrd 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( A -s ( 1s /su n ) )
71 breq12 
 |-  ( ( y = ( A -s ( 1s /su n ) ) /\ z = ( A +s ( 1s /su m ) ) ) -> ( y  ( A -s ( 1s /su n ) )
72 70 71 syl5ibrcom 
 |-  ( ( A e. No /\ ( n e. NN_s /\ m e. NN_s ) ) -> ( ( y = ( A -s ( 1s /su n ) ) /\ z = ( A +s ( 1s /su m ) ) ) -> y
73 72 rexlimdvva 
 |-  ( A e. No -> ( E. n e. NN_s E. m e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ z = ( A +s ( 1s /su m ) ) ) -> y
74 38 73 biimtrid 
 |-  ( A e. No -> ( ( y e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } /\ z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) -> y
75 74 3impib 
 |-  ( ( A e. No /\ y e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } /\ z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) -> y
76 3 5 16 22 75 ssltd 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <