Metamath Proof Explorer

Theorem negsid

Description: Surreal addition of a number and its negative. Theorem 4(iii) of Conway p. 17. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsid 
|- ( A e. No -> ( A +s ( -us ` A ) ) = 0s )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x = xO -> x = xO )
2 fveq2 
 |-  ( x = xO -> ( -us ` x ) = ( -us ` xO ) )
3 1 2 oveq12d 
 |-  ( x = xO -> ( x +s ( -us ` x ) ) = ( xO +s ( -us ` xO ) ) )
4 3 eqeq1d 
 |-  ( x = xO -> ( ( x +s ( -us ` x ) ) = 0s <-> ( xO +s ( -us ` xO ) ) = 0s ) )
5 id 
 |-  ( x = A -> x = A )
6 fveq2 
 |-  ( x = A -> ( -us ` x ) = ( -us ` A ) )
7 5 6 oveq12d 
 |-  ( x = A -> ( x +s ( -us ` x ) ) = ( A +s ( -us ` A ) ) )
8 7 eqeq1d 
 |-  ( x = A -> ( ( x +s ( -us ` x ) ) = 0s <-> ( A +s ( -us ` A ) ) = 0s ) )
9 lltropt 
 |-  ( _Left ` x ) <
10 9 a1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( _Left ` x ) <
11 negscut2 
 |-  ( x e. No -> ( -us " ( _Right ` x ) ) <
12 11 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( -us " ( _Right ` x ) ) <
13 lrcut 
 |-  ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
14 13 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
15 14 eqcomd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> x = ( ( _Left ` x ) |s ( _Right ` x ) ) )
16 negsval 
 |-  ( x e. No -> ( -us ` x ) = ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) )
17 16 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( -us ` x ) = ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) )
18 10 12 15 17 addsunif 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( x +s ( -us ` x ) ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) } ) ) )
19 negsfn 
 |-  -us Fn No
20 rightssno 
 |-  ( _Right ` x ) C_ No
21 oveq2 
 |-  ( p = ( -us ` xR ) -> ( x +s p ) = ( x +s ( -us ` xR ) ) )
22 21 eqeq2d 
 |-  ( p = ( -us ` xR ) -> ( b = ( x +s p ) <-> b = ( x +s ( -us ` xR ) ) ) )
23 22 rexima 
 |-  ( ( -us Fn No /\ ( _Right ` x ) C_ No ) -> ( E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) <-> E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) ) )
24 19 20 23 mp2an 
 |-  ( E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) <-> E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) )
25 24 abbii 
 |-  { b | E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) } = { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) }
26 25 uneq2i 
 |-  ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) } ) = ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } )
27 leftssno 
 |-  ( _Left ` x ) C_ No
28 oveq2 
 |-  ( q = ( -us ` xL ) -> ( x +s q ) = ( x +s ( -us ` xL ) ) )
29 28 eqeq2d 
 |-  ( q = ( -us ` xL ) -> ( d = ( x +s q ) <-> d = ( x +s ( -us ` xL ) ) ) )
30 29 rexima 
 |-  ( ( -us Fn No /\ ( _Left ` x ) C_ No ) -> ( E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) <-> E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) ) )
31 19 27 30 mp2an 
 |-  ( E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) <-> E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) )
32 31 abbii 
 |-  { d | E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) } = { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) }
33 32 uneq2i 
 |-  ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) } ) = ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } )
34 26 33 oveq12i 
 |-  ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) )
35 fvex 
 |-  ( _Left ` x ) e. _V
36 35 abrexex 
 |-  { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } e. _V
37 fvex 
 |-  ( _Right ` x ) e. _V
38 37 abrexex 
 |-  { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } e. _V
39 36 38 unex 
 |-  ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) e. _V
40 39 a1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) e. _V )
41 snex 
 |-  { 0s } e. _V
42 41 a1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { 0s } e. _V )
43 27 sseli 
 |-  ( xL e. ( _Left ` x ) -> xL e. No )
44 43 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> xL e. No )
45 simpll 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> x e. No )
46 45 negscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( -us ` x ) e. No )
47 44 46 addscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL +s ( -us ` x ) ) e. No )
48 eleq1 
 |-  ( a = ( xL +s ( -us ` x ) ) -> ( a e. No <-> ( xL +s ( -us ` x ) ) e. No ) )
49 47 48 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( a = ( xL +s ( -us ` x ) ) -> a e. No ) )
50 49 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) -> a e. No ) )
51 50 abssdv 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } C_ No )
52 simpll 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> x e. No )
53 20 sseli 
 |-  ( xR e. ( _Right ` x ) -> xR e. No )
54 53 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> xR e. No )
55 54 negscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( -us ` xR ) e. No )
56 52 55 addscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( x +s ( -us ` xR ) ) e. No )
57 eleq1 
 |-  ( b = ( x +s ( -us ` xR ) ) -> ( b e. No <-> ( x +s ( -us ` xR ) ) e. No ) )
58 56 57 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( b = ( x +s ( -us ` xR ) ) -> b e. No ) )
59 58 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) -> b e. No ) )
60 59 abssdv 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } C_ No )
61 51 60 unssd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) C_ No )
62 0sno 
 |-  0s e. No
63 snssi 
 |-  ( 0s e. No -> { 0s } C_ No )
64 62 63 mp1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { 0s } C_ No )
65 elun 
 |-  ( p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) <-> ( p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } \/ p e. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) )
66 vex 
 |-  p e. _V
67 eqeq1 
 |-  ( a = p -> ( a = ( xL +s ( -us ` x ) ) <-> p = ( xL +s ( -us ` x ) ) ) )
68 67 rexbidv 
 |-  ( a = p -> ( E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) <-> E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) ) )
69 66 68 elab 
 |-  ( p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } <-> E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) )
70 eqeq1 
 |-  ( b = p -> ( b = ( x +s ( -us ` xR ) ) <-> p = ( x +s ( -us ` xR ) ) ) )
71 70 rexbidv 
 |-  ( b = p -> ( E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) <-> E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) )
72 66 71 elab 
 |-  ( p e. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } <-> E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) )
73 69 72 orbi12i 
 |-  ( ( p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } \/ p e. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) <-> ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) \/ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) )
74 65 73 bitri 
 |-  ( p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) <-> ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) \/ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) )
75 velsn 
 |-  ( q e. { 0s } <-> q = 0s )
76 74 75 anbi12i 
 |-  ( ( p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) /\ q e. { 0s } ) <-> ( ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) \/ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) /\ q = 0s ) )
77 leftlt 
 |-  ( xL e. ( _Left ` x ) -> xL
78 77 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> xL
79 sltnegim 
 |-  ( ( xL e. No /\ x e. No ) -> ( xL  ( -us ` x )
80 44 45 79 syl2anc 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL  ( -us ` x )
81 78 80 mpd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( -us ` x )
82 44 negscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( -us ` xL ) e. No )
83 46 82 44 sltadd2d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( ( -us ` x )  ( xL +s ( -us ` x ) )
84 81 83 mpbid 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL +s ( -us ` x ) )
85 id 
 |-  ( xO = xL -> xO = xL )
86 fveq2 
 |-  ( xO = xL -> ( -us ` xO ) = ( -us ` xL ) )
87 85 86 oveq12d 
 |-  ( xO = xL -> ( xO +s ( -us ` xO ) ) = ( xL +s ( -us ` xL ) ) )
88 87 eqeq1d 
 |-  ( xO = xL -> ( ( xO +s ( -us ` xO ) ) = 0s <-> ( xL +s ( -us ` xL ) ) = 0s ) )
89 simplr 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s )
90 elun1 
 |-  ( xL e. ( _Left ` x ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
91 90 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
92 88 89 91 rspcdva 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL +s ( -us ` xL ) ) = 0s )
93 84 92 breqtrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL +s ( -us ` x ) )
94 breq1 
 |-  ( p = ( xL +s ( -us ` x ) ) -> ( p  ( xL +s ( -us ` x ) )
95 93 94 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( p = ( xL +s ( -us ` x ) ) -> p
96 95 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) -> p
97 96 imp 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) ) -> p
98 rightgt 
 |-  ( xR e. ( _Right ` x ) -> x
99 98 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> x
100 52 54 55 sltadd1d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( x  ( x +s ( -us ` xR ) )
101 99 100 mpbid 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( x +s ( -us ` xR ) )
102 id 
 |-  ( xO = xR -> xO = xR )
103 fveq2 
 |-  ( xO = xR -> ( -us ` xO ) = ( -us ` xR ) )
104 102 103 oveq12d 
 |-  ( xO = xR -> ( xO +s ( -us ` xO ) ) = ( xR +s ( -us ` xR ) ) )
105 104 eqeq1d 
 |-  ( xO = xR -> ( ( xO +s ( -us ` xO ) ) = 0s <-> ( xR +s ( -us ` xR ) ) = 0s ) )
106 simplr 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s )
107 elun2 
 |-  ( xR e. ( _Right ` x ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
108 107 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
109 105 106 108 rspcdva 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( xR +s ( -us ` xR ) ) = 0s )
110 101 109 breqtrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( x +s ( -us ` xR ) )
111 breq1 
 |-  ( p = ( x +s ( -us ` xR ) ) -> ( p  ( x +s ( -us ` xR ) )
112 110 111 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( p = ( x +s ( -us ` xR ) ) -> p
113 112 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) -> p
114 113 imp 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) -> p
115 97 114 jaodan 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) \/ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) ) -> p
116 breq2 
 |-  ( q = 0s -> ( p  p
117 115 116 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) \/ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) ) -> ( q = 0s -> p
118 117 expimpd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( ( E. xL e. ( _Left ` x ) p = ( xL +s ( -us ` x ) ) \/ E. xR e. ( _Right ` x ) p = ( x +s ( -us ` xR ) ) ) /\ q = 0s ) -> p
119 76 118 biimtrid 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) /\ q e. { 0s } ) -> p
120 119 3impib 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) /\ q e. { 0s } ) -> p
121 40 42 61 64 120 ssltd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) <
122 37 abrexex 
 |-  { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } e. _V
123 35 abrexex 
 |-  { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } e. _V
124 122 123 unex 
 |-  ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) e. _V
125 124 a1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) e. _V )
126 52 negscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( -us ` x ) e. No )
127 54 126 addscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( xR +s ( -us ` x ) ) e. No )
128 eleq1 
 |-  ( c = ( xR +s ( -us ` x ) ) -> ( c e. No <-> ( xR +s ( -us ` x ) ) e. No ) )
129 127 128 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( c = ( xR +s ( -us ` x ) ) -> c e. No ) )
130 129 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) -> c e. No ) )
131 130 abssdv 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } C_ No )
132 45 82 addscld 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( x +s ( -us ` xL ) ) e. No )
133 eleq1 
 |-  ( d = ( x +s ( -us ` xL ) ) -> ( d e. No <-> ( x +s ( -us ` xL ) ) e. No ) )
134 132 133 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( d = ( x +s ( -us ` xL ) ) -> d e. No ) )
135 134 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) -> d e. No ) )
136 135 abssdv 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } C_ No )
137 131 136 unssd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) C_ No )
138 velsn 
 |-  ( p e. { 0s } <-> p = 0s )
139 elun 
 |-  ( q e. ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) <-> ( q e. { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } \/ q e. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) )
140 vex 
 |-  q e. _V
141 eqeq1 
 |-  ( c = q -> ( c = ( xR +s ( -us ` x ) ) <-> q = ( xR +s ( -us ` x ) ) ) )
142 141 rexbidv 
 |-  ( c = q -> ( E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) <-> E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) ) )
143 140 142 elab 
 |-  ( q e. { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } <-> E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) )
144 eqeq1 
 |-  ( d = q -> ( d = ( x +s ( -us ` xL ) ) <-> q = ( x +s ( -us ` xL ) ) ) )
145 144 rexbidv 
 |-  ( d = q -> ( E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) <-> E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) )
146 140 145 elab 
 |-  ( q e. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } <-> E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) )
147 143 146 orbi12i 
 |-  ( ( q e. { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } \/ q e. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) <-> ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) )
148 139 147 bitri 
 |-  ( q e. ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) <-> ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) )
149 138 148 anbi12i 
 |-  ( ( p e. { 0s } /\ q e. ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) ) <-> ( p = 0s /\ ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) ) )
150 sltnegim 
 |-  ( ( x e. No /\ xR e. No ) -> ( x  ( -us ` xR )
151 52 54 150 syl2anc 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( x  ( -us ` xR )
152 99 151 mpd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( -us ` xR )
153 55 126 54 sltadd2d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( ( -us ` xR )  ( xR +s ( -us ` xR ) )
154 152 153 mpbid 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( xR +s ( -us ` xR ) )
155 109 154 eqbrtrrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> 0s
156 breq2 
 |-  ( q = ( xR +s ( -us ` x ) ) -> ( 0s  0s
157 155 156 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( q = ( xR +s ( -us ` x ) ) -> 0s
158 157 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) -> 0s
159 158 imp 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) ) -> 0s
160 44 45 82 sltadd1d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL  ( xL +s ( -us ` xL ) )
161 78 160 mpbid 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL +s ( -us ` xL ) )
162 92 161 eqbrtrrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> 0s
163 breq2 
 |-  ( q = ( x +s ( -us ` xL ) ) -> ( 0s  0s
164 162 163 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( q = ( x +s ( -us ` xL ) ) -> 0s
165 164 rexlimdva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) -> 0s
166 165 imp 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) -> 0s
167 159 166 jaodan 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) ) -> 0s
168 breq1 
 |-  ( p = 0s -> ( p  0s
169 167 168 syl5ibrcom 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) ) -> ( p = 0s -> p
170 169 ex 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) -> ( p = 0s -> p
171 170 impcomd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( p = 0s /\ ( E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) \/ E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) ) -> p
172 149 171 biimtrid 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( p e. { 0s } /\ q e. ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) ) -> p
173 172 3impib 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ p e. { 0s } /\ q e. ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) ) -> p
174 42 125 64 137 173 ssltd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { 0s } <
175 121 174 cuteq0 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. xR e. ( _Right ` x ) b = ( x +s ( -us ` xR ) ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } ) ) = 0s )
176 34 175 eqtrid 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s ( -us ` x ) ) } u. { b | E. p e. ( -us " ( _Right ` x ) ) b = ( x +s p ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } u. { d | E. q e. ( -us " ( _Left ` x ) ) d = ( x +s q ) } ) ) = 0s )
177 18 176 eqtrd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( x +s ( -us ` x ) ) = 0s )
178 177 ex 
 |-  ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s -> ( x +s ( -us ` x ) ) = 0s ) )
179 4 8 178 noinds 
 |-  ( A e. No -> ( A +s ( -us ` A ) ) = 0s )