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\in \mathrm{No}\to A{+}_s{+}_s\left(A\right)=0_s$$

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\to x=A$$
6		fveq2	$$⊢x=A\to {+}_s\left(x\right)={+}_s\left(A\right)$$
7	5 6	oveq12d	$$⊢x=A\to x{+}_s{+}_s\left(x\right)=A{+}_s{+}_s\left(A\right)$$
8	7	eqeq1d	$$⊢x=A\to \left(x{+}_s{+}_s\left(x\right)=0_s\leftrightarrow A{+}_s{+}_s\left(A\right)=0_s\right)$$
9		lltropt	$$⊢L\left(x\right){\ll }_{s}R\left(x\right)$$
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	$$⊢x\in \mathrm{No}\to {+}_s\left[R\left(x\right)\right]{\ll }_s{+}_s\left[L\left(x\right)\right]$$
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	$$⊢x\in \mathrm{No}\to L\left(x\right){|}_{s}R\left(x\right)=x$$
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	$$⊢x\in \mathrm{No}\to {+}_s\left(x\right)={+}_s\left[R\left(x\right)\right]{|}_s{+}_s\left[L\left(x\right)\right]$$
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	$$⊢{+}_{s}Fn\mathrm{No}$$
20		rightssno	$$⊢R\left(x\right)\subseteq \mathrm{No}$$
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	rexima	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	$$⊢L\left(x\right)\subseteq \mathrm{No}$$
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	rexima	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	$$⊢L\left(x\right)\in \mathrm{V}$$
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	$$⊢R\left(x\right)\in \mathrm{V}$$
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	$$⊢\left\{0_s\right\}\in \mathrm{V}$$
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	$$⊢0_s\in \mathrm{No}$$
63		snssi	$$⊢0_s\in \mathrm{No}\to \left\{0_s\right\}\subseteq \mathrm{No}$$
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\in \mathrm{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	$$⊢q\in \left\{0_s\right\}\leftrightarrow q=0_s$$
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		leftlt	Could not format ( xL e. ( _Left ` x ) -> xL xL
78	77	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
79		sltnegim	Could not format ( ( xL e. No /\ x e. No ) -> ( xL ( -us ` x ) ( xL ( -us ` x )
80	44 45 79	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 )
81	78 80	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 )
82	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 |-
83	46 82 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 ) )
84	81 83	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 ) )
85		id	Could not format ( xO = xL -> xO = xL ) : No typesetting found for |- ( xO = xL -> xO = xL ) with typecode |-
86		fveq2	Could not format ( xO = xL -> ( -us ` xO ) = ( -us ` xL ) ) : No typesetting found for |- ( xO = xL -> ( -us ` xO ) = ( -us ` xL ) ) with typecode |-
87	85 86	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 |-
88	87	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 |-
89		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 |-
90		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 |-
91	90	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 |-
92	88 89 91	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 |-
93	84 92	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 ) )
94		breq1	Could not format ( p = ( xL +s ( -us ` x ) ) -> ( p ( xL +s ( -us ` x ) ) ( p ( xL +s ( -us ` x ) )
95	93 94	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
96	95	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
97	96	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
98		rightgt	Could not format ( xR e. ( _Right ` x ) -> x x
99	98	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
100	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 ) )
101	99 100	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 ) )
102		id	Could not format ( xO = xR -> xO = xR ) : No typesetting found for |- ( xO = xR -> xO = xR ) with typecode |-
103		fveq2	Could not format ( xO = xR -> ( -us ` xO ) = ( -us ` xR ) ) : No typesetting found for |- ( xO = xR -> ( -us ` xO ) = ( -us ` xR ) ) with typecode |-
104	102 103	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 |-
105	104	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 |-
106		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 |-
107		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 |-
108	107	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 |-
109	105 106 108	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 |-
110	101 109	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 ) )
111		breq1	Could not format ( p = ( x +s ( -us ` xR ) ) -> ( p ( x +s ( -us ` xR ) ) ( p ( x +s ( -us ` xR ) )
112	110 111	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
113	112	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
114	113	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
115	97 114	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
116		breq2	$$⊢q=0_s\to \left(p{<}_{s}q\leftrightarrow p{<}_s{0}_s\right)$$
117	115 116	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
118	117	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
119	76 118	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
120	119	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
121	40 42 61 64 120	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 ) ) } ) <
122	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 |-
123	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 |-
124	122 123	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 |-
125	124	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 |-
126	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 |-
127	54 126	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 |-
128		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 |-
129	127 128	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 |-
130	129	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 |-
131	130	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 |-
132	45 82	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 |-
133		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 |-
134	132 133	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 |-
135	134	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 |-
136	135	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 |-
137	131 136	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 |-
138		velsn	$$⊢p\in \left\{0_s\right\}\leftrightarrow p=0_s$$
139		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 |-
140		vex	$$⊢q\in \mathrm{V}$$
141		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 |-
142	141	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 |-
143	140 142	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 |-
144		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 |-
145	144	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 |-
146	140 145	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 |-
147	143 146	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 |-
148	139 147	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 |-
149	138 148	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 |-
150		sltnegim	Could not format ( ( x e. No /\ xR e. No ) -> ( x ( -us ` xR ) ( x ( -us ` xR )
151	52 54 150	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 )
152	99 151	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 )
153	55 126 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 ) )
154	152 153	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 ) )
155	109 154	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
156		breq2	Could not format ( q = ( xR +s ( -us ` x ) ) -> ( 0s 0s ( 0s 0s
157	155 156	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
158	157	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
159	158	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
160	44 45 82	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 ) )
161	78 160	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 ) )
162	92 161	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
163		breq2	Could not format ( q = ( x +s ( -us ` xL ) ) -> ( 0s 0s ( 0s 0s
164	162 163	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
165	164	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
166	165	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
167	159 166	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
168		breq1	$$⊢p=0_s\to \left(p{<}_{s}q\leftrightarrow 0_s{<}_{s}q\right)$$
169	167 168	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
170	169	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
171	170	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
172	149 171	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
173	172	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
174	42 125 64 137 173	ssltd	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s ( -us ` xO ) ) = 0s ) -> { 0s } < { 0s } <
175	121 174	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 |-
176	34 175	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 |-
177	18 176	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 |-
178	177	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 |-
179	4 8 178	noinds	$$⊢A\in \mathrm{No}\to A{+}_s{+}_s\left(A\right)=0_s$$