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 imaeqsexv 
 |-  ( ( -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 imaeqsexv 
 |-  ( ( -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 leftval 
 |-  ( _Left ` x ) = { xL e. ( _Old ` ( bday ` x ) ) | xL
78 77 reqabi 
 |-  ( xL e. ( _Left ` x ) <-> ( xL e. ( _Old ` ( bday ` x ) ) /\ xL
79 78 simprbi 
 |-  ( xL e. ( _Left ` x ) -> xL
80 79 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> xL
81 sltnegim 
 |-  ( ( xL e. No /\ x e. No ) -> ( xL  ( -us ` x )
82 44 45 81 syl2anc 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( xL  ( -us ` x )
83 80 82 mpd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> ( -us ` x )
84 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 )
85 46 84 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 ) )
86 83 85 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 ) )
87 id 
 |-  ( xO = xL -> xO = xL )
88 fveq2 
 |-  ( xO = xL -> ( -us ` xO ) = ( -us ` xL ) )
89 87 88 oveq12d 
 |-  ( xO = xL -> ( xO +s ( -us ` xO ) ) = ( xL +s ( -us ` xL ) ) )
90 89 eqeq1d 
 |-  ( xO = xL -> ( ( xO +s ( -us ` xO ) ) = 0s <-> ( xL +s ( -us ` xL ) ) = 0s ) )
91 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 )
92 elun1 
 |-  ( xL e. ( _Left ` x ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
93 92 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 ) ) )
94 90 91 93 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 )
95 86 94 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 ) )
96 breq1 
 |-  ( p = ( xL +s ( -us ` x ) ) -> ( p  ( xL +s ( -us ` x ) )
97 95 96 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
98 97 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
99 98 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
100 rightval 
 |-  ( _Right ` x ) = { xR e. ( _Old ` ( bday ` x ) ) | x
101 100 reqabi 
 |-  ( xR e. ( _Right ` x ) <-> ( xR e. ( _Old ` ( bday ` x ) ) /\ x
102 101 simprbi 
 |-  ( xR e. ( _Right ` x ) -> x
103 102 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> x
104 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 ) )
105 103 104 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 ) )
106 id 
 |-  ( xO = xR -> xO = xR )
107 fveq2 
 |-  ( xO = xR -> ( -us ` xO ) = ( -us ` xR ) )
108 106 107 oveq12d 
 |-  ( xO = xR -> ( xO +s ( -us ` xO ) ) = ( xR +s ( -us ` xR ) ) )
109 108 eqeq1d 
 |-  ( xO = xR -> ( ( xO +s ( -us ` xO ) ) = 0s <-> ( xR +s ( -us ` xR ) ) = 0s ) )
110 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 )
111 elun2 
 |-  ( xR e. ( _Right ` x ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
112 111 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 ) ) )
113 109 110 112 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 )
114 105 113 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 ) )
115 breq1 
 |-  ( p = ( x +s ( -us ` xR ) ) -> ( p  ( x +s ( -us ` xR ) )
116 114 115 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
117 116 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
118 117 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
119 99 118 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
120 breq2 
 |-  ( q = 0s -> ( p  p
121 119 120 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
122 121 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
123 76 122 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
124 123 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
125 40 42 61 64 124 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 ) ) } ) <
126 37 abrexex 
 |-  { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } e. _V
127 35 abrexex 
 |-  { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } e. _V
128 126 127 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
129 128 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 )
130 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 )
131 54 130 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 )
132 eleq1 
 |-  ( c = ( xR +s ( -us ` x ) ) -> ( c e. No <-> ( xR +s ( -us ` x ) ) e. No ) )
133 131 132 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 ) )
134 133 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 ) )
135 134 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 )
136 45 84 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 )
137 eleq1 
 |-  ( d = ( x +s ( -us ` xL ) ) -> ( d e. No <-> ( x +s ( -us ` xL ) ) e. No ) )
138 136 137 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 ) )
139 138 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 ) )
140 139 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 )
141 135 140 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 )
142 velsn 
 |-  ( p e. { 0s } <-> p = 0s )
143 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 ) ) } ) )
144 vex 
 |-  q e. _V
145 eqeq1 
 |-  ( c = q -> ( c = ( xR +s ( -us ` x ) ) <-> q = ( xR +s ( -us ` x ) ) ) )
146 145 rexbidv 
 |-  ( c = q -> ( E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) <-> E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) ) )
147 144 146 elab 
 |-  ( q e. { c | E. xR e. ( _Right ` x ) c = ( xR +s ( -us ` x ) ) } <-> E. xR e. ( _Right ` x ) q = ( xR +s ( -us ` x ) ) )
148 eqeq1 
 |-  ( d = q -> ( d = ( x +s ( -us ` xL ) ) <-> q = ( x +s ( -us ` xL ) ) ) )
149 148 rexbidv 
 |-  ( d = q -> ( E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) <-> E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) ) )
150 144 149 elab 
 |-  ( q e. { d | E. xL e. ( _Left ` x ) d = ( x +s ( -us ` xL ) ) } <-> E. xL e. ( _Left ` x ) q = ( x +s ( -us ` xL ) ) )
151 147 150 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 ) ) ) )
152 143 151 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 ) ) ) )
153 142 152 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 ) ) ) ) )
154 sltnegim 
 |-  ( ( x e. No /\ xR e. No ) -> ( x  ( -us ` xR )
155 52 54 154 syl2anc 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( x  ( -us ` xR )
156 103 155 mpd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> ( -us ` xR )
157 55 130 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 ) )
158 156 157 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 ) )
159 113 158 eqbrtrrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xR e. ( _Right ` x ) ) -> 0s
160 breq2 
 |-  ( q = ( xR +s ( -us ` x ) ) -> ( 0s  0s
161 159 160 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
162 161 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
163 162 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
164 44 45 84 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 ) )
165 80 164 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 ) )
166 94 165 eqbrtrrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) /\ xL e. ( _Left ` x ) ) -> 0s
167 breq2 
 |-  ( q = ( x +s ( -us ` xL ) ) -> ( 0s  0s
168 166 167 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
169 168 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
170 169 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
171 163 170 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
172 breq1 
 |-  ( p = 0s -> ( p  0s
173 171 172 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
174 173 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
175 174 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
176 153 175 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
177 176 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
178 42 129 64 141 177 ssltd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { 0s } <
179 125 178 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 )
180 34 179 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 )
181 18 180 eqtrd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> ( x +s ( -us ` x ) ) = 0s )
182 181 ex 
 |-  ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s -> ( x +s ( -us ` x ) ) = 0s ) )
183 4 8 182 noinds 
 |-  ( A e. No -> ( A +s ( -us ` A ) ) = 0s )