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	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( B +s A ) )

Proof

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