Theorem addscom

Description: Surreal addition commutes. Part of Theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	addscom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=B{+}_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x +s y ) = ( xO +s y ) ) : No typesetting found for |- ( x = xO -> ( x +s y ) = ( xO +s y ) ) with typecode |-
2		oveq2	Could not format ( x = xO -> ( y +s x ) = ( y +s xO ) ) : No typesetting found for |- ( x = xO -> ( y +s x ) = ( y +s xO ) ) with typecode |-
3	1 2	eqeq12d	Could not format ( x = xO -> ( ( x +s y ) = ( y +s x ) <-> ( xO +s y ) = ( y +s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x +s y ) = ( y +s x ) <-> ( xO +s y ) = ( y +s xO ) ) ) with typecode |-
4		oveq2	Could not format ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) : No typesetting found for |- ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) with typecode |-
5		oveq1	Could not format ( y = yO -> ( y +s xO ) = ( yO +s xO ) ) : No typesetting found for |- ( y = yO -> ( y +s xO ) = ( yO +s xO ) ) with typecode |-
6	4 5	eqeq12d	Could not format ( y = yO -> ( ( xO +s y ) = ( y +s xO ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO +s y ) = ( y +s xO ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) with typecode |-
7		oveq1	Could not format ( x = xO -> ( x +s yO ) = ( xO +s yO ) ) : No typesetting found for |- ( x = xO -> ( x +s yO ) = ( xO +s yO ) ) with typecode |-
8		oveq2	Could not format ( x = xO -> ( yO +s x ) = ( yO +s xO ) ) : No typesetting found for |- ( x = xO -> ( yO +s x ) = ( yO +s xO ) ) with typecode |-
9	7 8	eqeq12d	Could not format ( x = xO -> ( ( x +s yO ) = ( yO +s x ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x +s yO ) = ( yO +s x ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) with typecode |-
10		oveq1	$$⊢x=A\to x{+}_{s}y=A{+}_{s}y$$
11		oveq2	$$⊢x=A\to y{+}_{s}x=y{+}_{s}A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(x{+}_{s}y=y{+}_{s}x\leftrightarrow A{+}_{s}y=y{+}_{s}A\right)$$
13		oveq2	$$⊢y=B\to A{+}_{s}y=A{+}_{s}B$$
14		oveq1	$$⊢y=B\to y{+}_{s}A=B{+}_{s}A$$
15	13 14	eqeq12d	$$⊢y=B\to \left(A{+}_{s}y=y{+}_{s}A\leftrightarrow A{+}_{s}B=B{+}_{s}A\right)$$
16		simpr2	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) ) with typecode |-
17		elun1	$$⊢l\in L\left(x\right)\to l\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
18		oveq1	Could not format ( xO = l -> ( xO +s y ) = ( l +s y ) ) : No typesetting found for |- ( xO = l -> ( xO +s y ) = ( l +s y ) ) with typecode |-
19		oveq2	Could not format ( xO = l -> ( y +s xO ) = ( y +s l ) ) : No typesetting found for |- ( xO = l -> ( y +s xO ) = ( y +s l ) ) with typecode |-
20	18 19	eqeq12d	Could not format ( xO = l -> ( ( xO +s y ) = ( y +s xO ) <-> ( l +s y ) = ( y +s l ) ) ) : No typesetting found for |- ( xO = l -> ( ( xO +s y ) = ( y +s xO ) <-> ( l +s y ) = ( y +s l ) ) ) with typecode |-
21	20	rspccva	Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ l e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( l +s y ) = ( y +s l ) ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ l e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( l +s y ) = ( y +s l ) ) with typecode |-
22	16 17 21	syl2an	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` x ) ) -> ( l +s y ) = ( y +s l ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` x ) ) -> ( l +s y ) = ( y +s l ) ) with typecode |-
23	22	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` x ) ) -> ( w = ( l +s y ) <-> w = ( y +s l ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` x ) ) -> ( w = ( l +s y ) <-> w = ( y +s l ) ) ) with typecode |-
24	23	rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _Left ` x ) w = ( l +s y ) <-> E. l e. ( _Left ` x ) w = ( y +s l ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _Left ` x ) w = ( l +s y ) <-> E. l e. ( _Left ` x ) w = ( y +s l ) ) ) with typecode |-
25	24	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. l e. ( _Left ` x ) w = ( l +s y ) } = { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. l e. ( _Left ` x ) w = ( l +s y ) } = { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) with typecode |-
26		simpr3	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) with typecode |-
27		elun1	$$⊢l\in L\left(y\right)\to l\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
28		oveq2	Could not format ( yO = l -> ( x +s yO ) = ( x +s l ) ) : No typesetting found for |- ( yO = l -> ( x +s yO ) = ( x +s l ) ) with typecode |-
29		oveq1	Could not format ( yO = l -> ( yO +s x ) = ( l +s x ) ) : No typesetting found for |- ( yO = l -> ( yO +s x ) = ( l +s x ) ) with typecode |-
30	28 29	eqeq12d	Could not format ( yO = l -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s l ) = ( l +s x ) ) ) : No typesetting found for |- ( yO = l -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s l ) = ( l +s x ) ) ) with typecode |-
31	30	rspccva	Could not format ( ( A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) /\ l e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) -> ( x +s l ) = ( l +s x ) ) : No typesetting found for |- ( ( A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) /\ l e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) -> ( x +s l ) = ( l +s x ) ) with typecode |-
32	26 27 31	syl2an	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` y ) ) -> ( x +s l ) = ( l +s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` y ) ) -> ( x +s l ) = ( l +s x ) ) with typecode |-
33	32	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` y ) ) -> ( z = ( x +s l ) <-> z = ( l +s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _Left ` y ) ) -> ( z = ( x +s l ) <-> z = ( l +s x ) ) ) with typecode |-
34	33	rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _Left ` y ) z = ( x +s l ) <-> E. l e. ( _Left ` y ) z = ( l +s x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _Left ` y ) z = ( x +s l ) <-> E. l e. ( _Left ` y ) z = ( l +s x ) ) ) with typecode |-
35	34	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. l e. ( _Left ` y ) z = ( x +s l ) } = { z | E. l e. ( _Left ` y ) z = ( l +s x ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. l e. ( _Left ` y ) z = ( x +s l ) } = { z | E. l e. ( _Left ` y ) z = ( l +s x ) } ) with typecode |-
36	25 35	uneq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) = ( { w | E. l e. ( _Left ` x ) w = ( y +s l ) } u. { z | E. l e. ( _Left ` y ) z = ( l +s x ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) = ( { w | E. l e. ( _Left ` x ) w = ( y +s l ) } u. { z | E. l e. ( _Left ` y ) z = ( l +s x ) } ) ) with typecode |-
37		uncom	$$⊢\left\{w|\exists l\in L\left(x\right)w=y{+}_{s}l\right\}\cup \left\{z|\exists l\in L\left(y\right)z=l{+}_{s}x\right\}=\left\{z|\exists l\in L\left(y\right)z=l{+}_{s}x\right\}\cup \left\{w|\exists l\in L\left(x\right)w=y{+}_{s}l\right\}$$
38	36 37	eqtrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) = ( { z | E. l e. ( _Left ` y ) z = ( l +s x ) } u. { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) = ( { z | E. l e. ( _Left ` y ) z = ( l +s x ) } u. { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) ) with typecode |-
39		elun2	$$⊢r\in R\left(x\right)\to r\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
40		oveq1	Could not format ( xO = r -> ( xO +s y ) = ( r +s y ) ) : No typesetting found for |- ( xO = r -> ( xO +s y ) = ( r +s y ) ) with typecode |-
41		oveq2	Could not format ( xO = r -> ( y +s xO ) = ( y +s r ) ) : No typesetting found for |- ( xO = r -> ( y +s xO ) = ( y +s r ) ) with typecode |-
42	40 41	eqeq12d	Could not format ( xO = r -> ( ( xO +s y ) = ( y +s xO ) <-> ( r +s y ) = ( y +s r ) ) ) : No typesetting found for |- ( xO = r -> ( ( xO +s y ) = ( y +s xO ) <-> ( r +s y ) = ( y +s r ) ) ) with typecode |-
43	42	rspccva	Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ r e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( r +s y ) = ( y +s r ) ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ r e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( r +s y ) = ( y +s r ) ) with typecode |-
44	16 39 43	syl2an	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` x ) ) -> ( r +s y ) = ( y +s r ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` x ) ) -> ( r +s y ) = ( y +s r ) ) with typecode |-
45	44	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` x ) ) -> ( w = ( r +s y ) <-> w = ( y +s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` x ) ) -> ( w = ( r +s y ) <-> w = ( y +s r ) ) ) with typecode |-
46	45	rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _Right ` x ) w = ( r +s y ) <-> E. r e. ( _Right ` x ) w = ( y +s r ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _Right ` x ) w = ( r +s y ) <-> E. r e. ( _Right ` x ) w = ( y +s r ) ) ) with typecode |-
47	46	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. r e. ( _Right ` x ) w = ( r +s y ) } = { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. r e. ( _Right ` x ) w = ( r +s y ) } = { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) with typecode |-
48		elun2	$$⊢r\in R\left(y\right)\to r\in \left(L\left(y\right)\cup R\left(y\right)\right)$$
49		oveq2	Could not format ( yO = r -> ( x +s yO ) = ( x +s r ) ) : No typesetting found for |- ( yO = r -> ( x +s yO ) = ( x +s r ) ) with typecode |-
50		oveq1	Could not format ( yO = r -> ( yO +s x ) = ( r +s x ) ) : No typesetting found for |- ( yO = r -> ( yO +s x ) = ( r +s x ) ) with typecode |-
51	49 50	eqeq12d	Could not format ( yO = r -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s r ) = ( r +s x ) ) ) : No typesetting found for |- ( yO = r -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s r ) = ( r +s x ) ) ) with typecode |-
52	51	rspccva	Could not format ( ( A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) /\ r e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) -> ( x +s r ) = ( r +s x ) ) : No typesetting found for |- ( ( A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) /\ r e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) -> ( x +s r ) = ( r +s x ) ) with typecode |-
53	26 48 52	syl2an	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` y ) ) -> ( x +s r ) = ( r +s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` y ) ) -> ( x +s r ) = ( r +s x ) ) with typecode |-
54	53	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` y ) ) -> ( z = ( x +s r ) <-> z = ( r +s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _Right ` y ) ) -> ( z = ( x +s r ) <-> z = ( r +s x ) ) ) with typecode |-
55	54	rexbidva	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _Right ` y ) z = ( x +s r ) <-> E. r e. ( _Right ` y ) z = ( r +s x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _Right ` y ) z = ( x +s r ) <-> E. r e. ( _Right ` y ) z = ( r +s x ) ) ) with typecode |-
56	55	abbidv	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. r e. ( _Right ` y ) z = ( x +s r ) } = { z | E. r e. ( _Right ` y ) z = ( r +s x ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. r e. ( _Right ` y ) z = ( x +s r ) } = { z | E. r e. ( _Right ` y ) z = ( r +s x ) } ) with typecode |-
57	47 56	uneq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) = ( { w | E. r e. ( _Right ` x ) w = ( y +s r ) } u. { z | E. r e. ( _Right ` y ) z = ( r +s x ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) = ( { w | E. r e. ( _Right ` x ) w = ( y +s r ) } u. { z | E. r e. ( _Right ` y ) z = ( r +s x ) } ) ) with typecode |-
58		uncom	$$⊢\left\{w|\exists r\in R\left(x\right)w=y{+}_{s}r\right\}\cup \left\{z|\exists r\in R\left(y\right)z=r{+}_{s}x\right\}=\left\{z|\exists r\in R\left(y\right)z=r{+}_{s}x\right\}\cup \left\{w|\exists r\in R\left(x\right)w=y{+}_{s}r\right\}$$
59	57 58	eqtrdi	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) = ( { z | E. r e. ( _Right ` y ) z = ( r +s x ) } u. { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) = ( { z | E. r e. ( _Right ` y ) z = ( r +s x ) } u. { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) ) with typecode |-
60	38 59	oveq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) ) = ( ( { z | E. l e. ( _Left ` y ) z = ( l +s x ) } u. { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _Right ` y ) z = ( r +s x ) } u. { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) ) = ( ( { z | E. l e. ( _Left ` y ) z = ( l +s x ) } u. { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _Right ` y ) z = ( r +s x ) } u. { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) ) ) with typecode |-
61		addsval	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to x{+}_{s}y=\left(\left\{w|\exists l\in L\left(x\right)w=l{+}_{s}y\right\}\cup \left\{z|\exists l\in L\left(y\right)z=x{+}_{s}l\right\}\right){|}_s\left(\left\{w|\exists r\in R\left(x\right)w=r{+}_{s}y\right\}\cup \left\{z|\exists r\in R\left(y\right)z=x{+}_{s}r\right\}\right)$$
62	61	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( ( { w | E. l e. ( _Left ` x ) w = ( l +s y ) } u. { z | E. l e. ( _Left ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _Right ` x ) w = ( r +s y ) } u. { z | E. r e. ( _Right ` y ) z = ( x +s r ) } ) ) ) with typecode |-
63		addsval	$$⊢\left(y\in \mathrm{No}\wedge x\in \mathrm{No}\right)\to y{+}_{s}x=\left(\left\{z|\exists l\in L\left(y\right)z=l{+}_{s}x\right\}\cup \left\{w|\exists l\in L\left(x\right)w=y{+}_{s}l\right\}\right){|}_s\left(\left\{z|\exists r\in R\left(y\right)z=r{+}_{s}x\right\}\cup \left\{w|\exists r\in R\left(x\right)w=y{+}_{s}r\right\}\right)$$
64	63	ancoms	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to y{+}_{s}x=\left(\left\{z|\exists l\in L\left(y\right)z=l{+}_{s}x\right\}\cup \left\{w|\exists l\in L\left(x\right)w=y{+}_{s}l\right\}\right){|}_s\left(\left\{z|\exists r\in R\left(y\right)z=r{+}_{s}x\right\}\cup \left\{w|\exists r\in R\left(x\right)w=y{+}_{s}r\right\}\right)$$
65	64	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( y +s x ) = ( ( { z | E. l e. ( _Left ` y ) z = ( l +s x ) } u. { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _Right ` y ) z = ( r +s x ) } u. { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( y +s x ) = ( ( { z | E. l e. ( _Left ` y ) z = ( l +s x ) } u. { w | E. l e. ( _Left ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _Right ` y ) z = ( r +s x ) } u. { w | E. r e. ( _Right ` x ) w = ( y +s r ) } ) ) ) with typecode |-
66	60 62 65	3eqtr4d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( y +s x ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( y +s x ) ) with typecode |-
67	66	ex	Could not format ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) -> ( x +s y ) = ( y +s x ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x +s yO ) = ( yO +s x ) ) -> ( x +s y ) = ( y +s x ) ) ) with typecode |-
68	3 6 9 12 15 67	no2inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{+}_{s}B=B{+}_{s}A$$