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 
|- ( ph -> L <
negsunif.2 
|- ( ph -> A = ( L |s R ) )
Assertion negsunif 
|- ( ph -> ( -us ` A ) = ( ( -us " R ) |s ( -us " L ) ) )

Proof

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