Metamath Proof Explorer

Theorem negsproplem2

Description: Lemma for surreal negation. Show that the cut that defines negation is legitimate. (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses negsproplem.1 
|- ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
negsproplem2.1 
|- ( ph -> A e. No )
Assertion negsproplem2 
|- ( ph -> ( -us " ( _Right ` A ) ) <

Proof

Step Hyp Ref Expression
1 negsproplem.1 
 |-  ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
2 negsproplem2.1 
 |-  ( ph -> A e. No )
3 negsfn 
 |-  -us Fn No
4 fnfun 
 |-  ( -us Fn No -> Fun -us )
5 3 4 ax-mp 
 |-  Fun -us
6 fvex 
 |-  ( _Right ` A ) e. _V
7 6 funimaex 
 |-  ( Fun -us -> ( -us " ( _Right ` A ) ) e. _V )
8 5 7 mp1i 
 |-  ( ph -> ( -us " ( _Right ` A ) ) e. _V )
9 fvex 
 |-  ( _Left ` A ) e. _V
10 9 funimaex 
 |-  ( Fun -us -> ( -us " ( _Left ` A ) ) e. _V )
11 5 10 mp1i 
 |-  ( ph -> ( -us " ( _Left ` A ) ) e. _V )
12 rightssold 
 |-  ( _Right ` A ) C_ ( _Old ` ( bday ` A ) )
13 imass2 
 |-  ( ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) -> ( -us " ( _Right ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) )
14 12 13 ax-mp 
 |-  ( -us " ( _Right ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) )
15 1 adantr 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
16 oldssno 
 |-  ( _Old ` ( bday ` A ) ) C_ No
17 16 sseli 
 |-  ( a e. ( _Old ` ( bday ` A ) ) -> a e. No )
18 17 adantl 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> a e. No )
19 0sno 
 |-  0s e. No
20 19 a1i 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> 0s e. No )
21 bday0s 
 |-  ( bday ` 0s ) = (/)
22 21 uneq2i 
 |-  ( ( bday ` a ) u. ( bday ` 0s ) ) = ( ( bday ` a ) u. (/) )
23 un0 
 |-  ( ( bday ` a ) u. (/) ) = ( bday ` a )
24 22 23 eqtri 
 |-  ( ( bday ` a ) u. ( bday ` 0s ) ) = ( bday ` a )
25 oldbdayim 
 |-  ( a e. ( _Old ` ( bday ` A ) ) -> ( bday ` a ) e. ( bday ` A ) )
26 25 adantl 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( bday ` a ) e. ( bday ` A ) )
27 elun1 
 |-  ( ( bday ` a ) e. ( bday ` A ) -> ( bday ` a ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
28 26 27 syl 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( bday ` a ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
29 24 28 eqeltrid 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( ( bday ` a ) u. ( bday ` 0s ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
30 15 18 20 29 negsproplem1 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( ( -us ` a ) e. No /\ ( a  ( -us ` 0s )
31 30 simpld 
 |-  ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( -us ` a ) e. No )
32 31 ralrimiva 
 |-  ( ph -> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No )
33 3 fndmi 
 |-  dom -us = No
34 16 33 sseqtrri 
 |-  ( _Old ` ( bday ` A ) ) C_ dom -us
35 funimass4 
 |-  ( ( Fun -us /\ ( _Old ` ( bday ` A ) ) C_ dom -us ) -> ( ( -us " ( _Old ` ( bday ` A ) ) ) C_ No <-> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) )
36 5 34 35 mp2an 
 |-  ( ( -us " ( _Old ` ( bday ` A ) ) ) C_ No <-> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No )
37 32 36 sylibr 
 |-  ( ph -> ( -us " ( _Old ` ( bday ` A ) ) ) C_ No )
38 14 37 sstrid 
 |-  ( ph -> ( -us " ( _Right ` A ) ) C_ No )
39 leftssold 
 |-  ( _Left ` A ) C_ ( _Old ` ( bday ` A ) )
40 imass2 
 |-  ( ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) -> ( -us " ( _Left ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) )
41 39 40 ax-mp 
 |-  ( -us " ( _Left ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) )
42 41 37 sstrid 
 |-  ( ph -> ( -us " ( _Left ` A ) ) C_ No )
43 rightssno 
 |-  ( _Right ` A ) C_ No
44 fvelimab 
 |-  ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) )
45 3 43 44 mp2an 
 |-  ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a )
46 leftssno 
 |-  ( _Left ` A ) C_ No
47 fvelimab 
 |-  ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) )
48 3 46 47 mp2an 
 |-  ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b )
49 45 48 anbi12i 
 |-  ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) )
50 reeanv 
 |-  ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) )
51 49 50 bitr4i 
 |-  ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) )
52 lltropt 
 |-  ( _Left ` A ) <
53 52 a1i 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( _Left ` A ) <
54 simprr 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Left ` A ) )
55 simprl 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Right ` A ) )
56 53 54 55 ssltsepcd 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL
57 1 adantr 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
58 46 sseli 
 |-  ( xL e. ( _Left ` A ) -> xL e. No )
59 58 ad2antll 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. No )
60 43 sseli 
 |-  ( xR e. ( _Right ` A ) -> xR e. No )
61 60 adantr 
 |-  ( ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) -> xR e. No )
62 61 adantl 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. No )
63 39 sseli 
 |-  ( xL e. ( _Left ` A ) -> xL e. ( _Old ` ( bday ` A ) ) )
64 63 ad2antll 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Old ` ( bday ` A ) ) )
65 oldbdayim 
 |-  ( xL e. ( _Old ` ( bday ` A ) ) -> ( bday ` xL ) e. ( bday ` A ) )
66 64 65 syl 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xL ) e. ( bday ` A ) )
67 12 a1i 
 |-  ( ph -> ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) )
68 67 sselda 
 |-  ( ( ph /\ xR e. ( _Right ` A ) ) -> xR e. ( _Old ` ( bday ` A ) ) )
69 68 adantrr 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Old ` ( bday ` A ) ) )
70 oldbdayim 
 |-  ( xR e. ( _Old ` ( bday ` A ) ) -> ( bday ` xR ) e. ( bday ` A ) )
71 69 70 syl 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xR ) e. ( bday ` A ) )
72 bdayelon 
 |-  ( bday ` xL ) e. On
73 bdayelon 
 |-  ( bday ` xR ) e. On
74 bdayelon 
 |-  ( bday ` A ) e. On
75 onunel 
 |-  ( ( ( bday ` xL ) e. On /\ ( bday ` xR ) e. On /\ ( bday ` A ) e. On ) -> ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) )
76 72 73 74 75 mp3an 
 |-  ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) )
77 66 71 76 sylanbrc 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) )
78 elun1 
 |-  ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
79 77 78 syl 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
80 57 59 62 79 negsproplem1 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( -us ` xL ) e. No /\ ( xL  ( -us ` xR )
81 80 simprd 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( xL  ( -us ` xR )
82 56 81 mpd 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( -us ` xR )
83 breq12 
 |-  ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> ( ( -us ` xR )  a
84 82 83 syl5ibcom 
 |-  ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a
85 84 rexlimdvva 
 |-  ( ph -> ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a
86 51 85 biimtrid 
 |-  ( ph -> ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) -> a
87 86 3impib 
 |-  ( ( ph /\ a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) -> a
88 8 11 38 42 87 ssltd 
 |-  ( ph -> ( -us " ( _Right ` A ) ) <