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 Could not format assertion : No typesetting found for |- ( A e. No -> ( A +s ( -us ` A ) ) = 0s ) with typecode |-

Proof

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