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