Metamath Proof Explorer


Theorem negsunif

Description: Uniformity property for surreal negation. If L and R are any cut that represents A , then they may be used instead of (LeftA ) and ( RightA ) in the definition of negation. (Contributed by Scott Fenton, 14-Feb-2025)

Ref Expression
Hypotheses negsunif.1 φ L s R
negsunif.2 φ A = L | s R
Assertion negsunif φ + s A = + s R | s + s L

Proof

Step Hyp Ref Expression
1 negsunif.1 φ L s R
2 negsunif.2 φ A = L | s R
3 1 scutcld φ L | s R No
4 2 3 eqeltrd φ A No
5 negsval A No + s A = + s R A | s + s L A
6 4 5 syl φ + s A = + s R A | s + s L A
7 negscut2 A No + s R A s + s L A
8 4 7 syl φ + s R A s + s L A
9 1 2 cofcutr2d φ c R A d R d s c
10 negsfn + s Fn No
11 ssltss2 L s R R No
12 1 11 syl φ R No
13 breq2 b = + s d + s c s b + s c s + s d
14 13 imaeqsexv + s Fn No R No b + s R + s c s b d R + s c s + s d
15 10 12 14 sylancr φ b + s R + s c s b d R + s c s + s d
16 15 ralbidv φ c R A b + s R + s c s b c R A d R + s c s + s d
17 12 adantr φ c R A R No
18 17 sselda φ c R A d R d No
19 rightssno R A No
20 19 sseli c R A c No
21 20 ad2antlr φ c R A d R c No
22 18 21 slenegd φ c R A d R d s c + s c s + s d
23 22 rexbidva φ c R A d R d s c d R + s c s + s d
24 23 ralbidva φ c R A d R d s c c R A d R + s c s + s d
25 16 24 bitr4d φ c R A b + s R + s c s b c R A d R d s c
26 9 25 mpbird φ c R A b + s R + s c s b
27 breq1 a = + s c a s b + s c s b
28 27 rexbidv a = + s c b + s R a s b b + s R + s c s b
29 28 imaeqsalv + s Fn No R A No a + s R A b + s R a s b c R A b + s R + s c s b
30 10 19 29 mp2an a + s R A b + s R a s b c R A b + s R + s c s b
31 26 30 sylibr φ a + s R A b + s R a s b
32 1 2 cofcutr1d φ c L A d L c s d
33 ssltss1 L s R L No
34 1 33 syl φ L No
35 breq1 b = + s d b s + s c + s d s + s c
36 35 imaeqsexv + s Fn No L No b + s L b s + s c d L + s d s + s c
37 10 34 36 sylancr φ b + s L b s + s c d L + s d s + s c
38 37 ralbidv φ c L A b + s L b s + s c c L A d L + s d s + s c
39 leftssno L A No
40 39 sseli c L A c No
41 40 ad2antlr φ c L A d L c No
42 34 adantr φ c L A L No
43 42 sselda φ c L A d L d No
44 41 43 slenegd φ c L A d L c s d + s d s + s c
45 44 rexbidva φ c L A d L c s d d L + s d s + s c
46 45 ralbidva φ c L A d L c s d c L A d L + s d s + s c
47 38 46 bitr4d φ c L A b + s L b s + s c c L A d L c s d
48 32 47 mpbird φ c L A b + s L b s + s c
49 breq2 a = + s c b s a b s + s c
50 49 rexbidv a = + s c b + s L b s a b + s L b s + s c
51 50 imaeqsalv + s Fn No L A No a + s L A b + s L b s a c L A b + s L b s + s c
52 10 39 51 mp2an a + s L A b + s L b s a c L A b + s L b s + s c
53 48 52 sylibr φ a + s L A b + s L b s a
54 fnfun + s Fn No Fun + s
55 10 54 ax-mp Fun + s
56 ssltex2 L s R R V
57 1 56 syl φ R V
58 funimaexg Fun + s R V + s R V
59 55 57 58 sylancr φ + s R V
60 snex + s A V
61 60 a1i φ + s A V
62 imassrn + s R ran + s
63 negsfo + s : No onto No
64 forn + s : No onto No ran + s = No
65 63 64 ax-mp ran + s = No
66 62 65 sseqtri + s R No
67 66 a1i φ + s R No
68 4 negscld φ + s A No
69 68 snssd φ + s A No
70 velsn a + s A a = + s A
71 fvelimab + s Fn No R No b + s R d R + s d = b
72 10 12 71 sylancr φ b + s R d R + s d = b
73 2 sneqd φ A = L | s R
74 73 adantr φ d R A = L | s R
75 scutcut L s R L | s R No L s L | s R L | s R s R
76 1 75 syl φ L | s R No L s L | s R L | s R s R
77 76 simp3d φ L | s R s R
78 77 adantr φ d R L | s R s R
79 74 78 eqbrtrd φ d R A s R
80 snidg A No A A
81 4 80 syl φ A A
82 81 adantr φ d R A A
83 simpr φ d R d R
84 79 82 83 ssltsepcd φ d R A < s d
85 4 adantr φ d R A No
86 12 sselda φ d R d No
87 85 86 sltnegd φ d R A < s d + s d < s + s A
88 84 87 mpbid φ d R + s d < s + s A
89 breq1 + s d = b + s d < s + s A b < s + s A
90 88 89 syl5ibcom φ d R + s d = b b < s + s A
91 90 rexlimdva φ d R + s d = b b < s + s A
92 72 91 sylbid φ b + s R b < s + s A
93 breq2 a = + s A b < s a b < s + s A
94 93 imbi2d a = + s A b + s R b < s a b + s R b < s + s A
95 92 94 syl5ibrcom φ a = + s A b + s R b < s a
96 70 95 biimtrid φ a + s A b + s R b < s a
97 96 3imp φ a + s A b + s R b < s a
98 97 3com23 φ b + s R a + s A b < s a
99 59 61 67 69 98 ssltd φ + s R s + s A
100 6 sneqd φ + s A = + s R A | s + s L A
101 99 100 breqtrd φ + s R s + s R A | s + s L A
102 ssltex1 L s R L V
103 1 102 syl φ L V
104 funimaexg Fun + s L V + s L V
105 55 103 104 sylancr φ + s L V
106 imassrn + s L ran + s
107 106 65 sseqtri + s L No
108 107 a1i φ + s L No
109 fvelimab + s Fn No L No b + s L c L + s c = b
110 10 34 109 sylancr φ b + s L c L + s c = b
111 1 adantr φ c L L s R
112 111 75 syl φ c L L | s R No L s L | s R L | s R s R
113 112 simp2d φ c L L s L | s R
114 73 adantr φ c L A = L | s R
115 113 114 breqtrrd φ c L L s A
116 simpr φ c L c L
117 81 adantr φ c L A A
118 115 116 117 ssltsepcd φ c L c < s A
119 34 sselda φ c L c No
120 4 adantr φ c L A No
121 119 120 sltnegd φ c L c < s A + s A < s + s c
122 118 121 mpbid φ c L + s A < s + s c
123 breq2 + s c = b + s A < s + s c + s A < s b
124 122 123 syl5ibcom φ c L + s c = b + s A < s b
125 124 rexlimdva φ c L + s c = b + s A < s b
126 110 125 sylbid φ b + s L + s A < s b
127 breq1 a = + s A a < s b + s A < s b
128 127 imbi2d a = + s A b + s L a < s b b + s L + s A < s b
129 126 128 syl5ibrcom φ a = + s A b + s L a < s b
130 70 129 biimtrid φ a + s A b + s L a < s b
131 130 3imp φ a + s A b + s L a < s b
132 61 105 69 108 131 ssltd φ + s A s + s L
133 100 132 eqbrtrrd φ + s R A | s + s L A s + s L
134 8 31 53 101 133 cofcut1d φ + s R A | s + s L A = + s R | s + s L
135 6 134 eqtrd φ + s A = + s R | s + s L