Theorem addsov

Description: The value of surreal addition. Definition from Conway p. 5. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	addsov	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-adds	|- +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) )
2	1	norec2ov	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) )
3		opex	|- <. A , B >. e. _V
4		addsfn	|- +s Fn ( No X. No )
5		fnfun	|- ( +s Fn ( No X. No ) -> Fun +s )
6	4 5	ax-mp	|- Fun +s
7		fvex	|- ( _L ` A ) e. _V
8		fvex	|- ( _R ` A ) e. _V
9	7 8	unex	|- ( ( _L ` A ) u. ( _R ` A ) ) e. _V
10		snex	|- { A } e. _V
11	9 10	unex	|- ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) e. _V
12		fvex	|- ( _L ` B ) e. _V
13		fvex	|- ( _R ` B ) e. _V
14	12 13	unex	|- ( ( _L ` B ) u. ( _R ` B ) ) e. _V
15		snex	|- { B } e. _V
16	14 15	unex	|- ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) e. _V
17	11 16	xpex	|- ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) e. _V
18	17	difexi	|- ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V
19		resfunexg	|- ( ( Fun +s /\ ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V ) -> ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V )
20	6 18 19	mp2an	|- ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V
21		2fveq3	|- ( x = <. A , B >. -> ( _L ` ( 1st ` x ) ) = ( _L ` ( 1st ` <. A , B >. ) ) )
22		fveq2	|- ( x = <. A , B >. -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) )
23	22	oveq2d	|- ( x = <. A , B >. -> ( l a ( 2nd ` x ) ) = ( l a ( 2nd ` <. A , B >. ) ) )
24	23	eqeq2d	|- ( x = <. A , B >. -> ( y = ( l a ( 2nd ` x ) ) <-> y = ( l a ( 2nd ` <. A , B >. ) ) ) )
25	21 24	rexeqbidv	|- ( x = <. A , B >. -> ( E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) <-> E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) ) )
26	25	abbidv	|- ( x = <. A , B >. -> { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } = { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } )
27		2fveq3	|- ( x = <. A , B >. -> ( _L ` ( 2nd ` x ) ) = ( _L ` ( 2nd ` <. A , B >. ) ) )
28		fveq2	|- ( x = <. A , B >. -> ( 1st ` x ) = ( 1st ` <. A , B >. ) )
29	28	oveq1d	|- ( x = <. A , B >. -> ( ( 1st ` x ) a l ) = ( ( 1st ` <. A , B >. ) a l ) )
30	29	eqeq2d	|- ( x = <. A , B >. -> ( z = ( ( 1st ` x ) a l ) <-> z = ( ( 1st ` <. A , B >. ) a l ) ) )
31	27 30	rexeqbidv	|- ( x = <. A , B >. -> ( E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) <-> E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) ) )
32	31	abbidv	|- ( x = <. A , B >. -> { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } = { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } )
33	26 32	uneq12d	|- ( x = <. A , B >. -> ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) = ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) )
34		2fveq3	|- ( x = <. A , B >. -> ( _R ` ( 1st ` x ) ) = ( _R ` ( 1st ` <. A , B >. ) ) )
35	22	oveq2d	|- ( x = <. A , B >. -> ( r a ( 2nd ` x ) ) = ( r a ( 2nd ` <. A , B >. ) ) )
36	35	eqeq2d	|- ( x = <. A , B >. -> ( y = ( r a ( 2nd ` x ) ) <-> y = ( r a ( 2nd ` <. A , B >. ) ) ) )
37	34 36	rexeqbidv	|- ( x = <. A , B >. -> ( E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) <-> E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) ) )
38	37	abbidv	|- ( x = <. A , B >. -> { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } = { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } )
39		2fveq3	|- ( x = <. A , B >. -> ( _R ` ( 2nd ` x ) ) = ( _R ` ( 2nd ` <. A , B >. ) ) )
40	28	oveq1d	|- ( x = <. A , B >. -> ( ( 1st ` x ) a r ) = ( ( 1st ` <. A , B >. ) a r ) )
41	40	eqeq2d	|- ( x = <. A , B >. -> ( z = ( ( 1st ` x ) a r ) <-> z = ( ( 1st ` <. A , B >. ) a r ) ) )
42	39 41	rexeqbidv	|- ( x = <. A , B >. -> ( E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) <-> E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) ) )
43	42	abbidv	|- ( x = <. A , B >. -> { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } = { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } )
44	38 43	uneq12d	|- ( x = <. A , B >. -> ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) = ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) )
45	33 44	oveq12d	|- ( x = <. A , B >. -> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) )
46		oveq	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( l a ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) )
47	46	eqeq2d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( l a ( 2nd ` <. A , B >. ) ) <-> y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) )
48	47	rexbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) )
49	48	abbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } )
50		oveq	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a l ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) )
51	50	eqeq2d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a l ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) )
52	51	rexbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) <-> E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) )
53	52	abbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } = { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } )
54	49 53	uneq12d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) = ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) )
55		oveq	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( r a ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) )
56	55	eqeq2d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( r a ( 2nd ` <. A , B >. ) ) <-> y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) )
57	56	rexbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) )
58	57	abbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } )
59		oveq	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a r ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) )
60	59	eqeq2d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a r ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) )
61	60	rexbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) <-> E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) )
62	61	abbidv	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } = { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } )
63	58 62	uneq12d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) = ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) )
64	54 63	oveq12d	|- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) )
65		eqid	|- ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) = ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) )
66		ovex	|- ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) e. _V
67	45 64 65 66	ovmpo	|- ( ( <. A , B >. e. _V /\ ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) )
68	3 20 67	mp2an	|- ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) )
69		op1stg	|- ( ( A e. No /\ B e. No ) -> ( 1st ` <. A , B >. ) = A )
70	69	fveq2d	|- ( ( A e. No /\ B e. No ) -> ( _L ` ( 1st ` <. A , B >. ) ) = ( _L ` A ) )
71	70	eleq2d	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` ( 1st ` <. A , B >. ) ) <-> l e. ( _L ` A ) ) )
72		op2ndg	|- ( ( A e. No /\ B e. No ) -> ( 2nd ` <. A , B >. ) = B )
73	72	adantr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( 2nd ` <. A , B >. ) = B )
74	73	oveq2d	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) )
75		elun1	|- ( l e. ( _L ` A ) -> l e. ( ( _L ` A ) u. ( _R ` A ) ) )
76		elun1	|- ( l e. ( ( _L ` A ) u. ( _R ` A ) ) -> l e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
77	75 76	syl	|- ( l e. ( _L ` A ) -> l e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
78	77	adantl	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> l e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
79		snidg	|- ( B e. No -> B e. { B } )
80		elun2	|- ( B e. { B } -> B e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
81	79 80	syl	|- ( B e. No -> B e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
82	81	adantl	|- ( ( A e. No /\ B e. No ) -> B e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
83	82	adantr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> B e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
84	78 83	opelxpd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> <. l , B >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) )
85		leftirr	|- ( A e. No -> -. A e. ( _L ` A ) )
86	85	adantr	|- ( ( A e. No /\ B e. No ) -> -. A e. ( _L ` A ) )
87		eleq1	|- ( l = A -> ( l e. ( _L ` A ) <-> A e. ( _L ` A ) ) )
88	87	notbid	|- ( l = A -> ( -. l e. ( _L ` A ) <-> -. A e. ( _L ` A ) ) )
89	86 88	syl5ibrcom	|- ( ( A e. No /\ B e. No ) -> ( l = A -> -. l e. ( _L ` A ) ) )
90	89	necon2ad	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` A ) -> l =/= A ) )
91	90	imp	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> l =/= A )
92	91	orcd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l =/= A \/ B =/= B ) )
93		simpr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> l e. ( _L ` A ) )
94		simplr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> B e. No )
95		opthneg	|- ( ( l e. ( _L ` A ) /\ B e. No ) -> ( <. l , B >. =/= <. A , B >. <-> ( l =/= A \/ B =/= B ) ) )
96	93 94 95	syl2anc	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( <. l , B >. =/= <. A , B >. <-> ( l =/= A \/ B =/= B ) ) )
97	92 96	mpbird	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> <. l , B >. =/= <. A , B >. )
98		eldifsn	|- ( <. l , B >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. l , B >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) /\ <. l , B >. =/= <. A , B >. ) )
99	84 97 98	sylanbrc	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> <. l , B >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )
100	99	fvresd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) = ( +s ` <. l , B >. ) )
101		df-ov	|- ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. )
102		df-ov	|- ( l +s B ) = ( +s ` <. l , B >. )
103	100 101 102	3eqtr4g	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( l +s B ) )
104	74 103	eqtrd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l +s B ) )
105	104	eqeq2d	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) )
106	105	ex	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` A ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) )
107	71 106	sylbid	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` ( 1st ` <. A , B >. ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) )
108	107	imp	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) )
109	70 108	rexeqbidva	|- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _L ` A ) y = ( l +s B ) ) )
110	109	abbidv	|- ( ( A e. No /\ B e. No ) -> { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _L ` A ) y = ( l +s B ) } )
111	72	fveq2d	|- ( ( A e. No /\ B e. No ) -> ( _L ` ( 2nd ` <. A , B >. ) ) = ( _L ` B ) )
112	111	eleq2d	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` ( 2nd ` <. A , B >. ) ) <-> l e. ( _L ` B ) ) )
113	69	adantr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( 1st ` <. A , B >. ) = A )
114	113	oveq1d	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) )
115		snidg	|- ( A e. No -> A e. { A } )
116	115	adantr	|- ( ( A e. No /\ B e. No ) -> A e. { A } )
117		elun2	|- ( A e. { A } -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
118	116 117	syl	|- ( ( A e. No /\ B e. No ) -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
119	118	adantr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
120		elun1	|- ( l e. ( _L ` B ) -> l e. ( ( _L ` B ) u. ( _R ` B ) ) )
121		elun1	|- ( l e. ( ( _L ` B ) u. ( _R ` B ) ) -> l e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
122	120 121	syl	|- ( l e. ( _L ` B ) -> l e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
123	122	adantl	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> l e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
124	119 123	opelxpd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> <. A , l >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) )
125		leftirr	|- ( B e. No -> -. B e. ( _L ` B ) )
126	125	adantl	|- ( ( A e. No /\ B e. No ) -> -. B e. ( _L ` B ) )
127		eleq1	|- ( l = B -> ( l e. ( _L ` B ) <-> B e. ( _L ` B ) ) )
128	127	notbid	|- ( l = B -> ( -. l e. ( _L ` B ) <-> -. B e. ( _L ` B ) ) )
129	126 128	syl5ibrcom	|- ( ( A e. No /\ B e. No ) -> ( l = B -> -. l e. ( _L ` B ) ) )
130	129	necon2ad	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` B ) -> l =/= B ) )
131	130	imp	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> l =/= B )
132	131	olcd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( A =/= A \/ l =/= B ) )
133		opthneg	|- ( ( A e. No /\ l e. ( _L ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) )
134	133	adantlr	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) )
135	132 134	mpbird	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> <. A , l >. =/= <. A , B >. )
136		eldifsn	|- ( <. A , l >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. A , l >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) /\ <. A , l >. =/= <. A , B >. ) )
137	124 135 136	sylanbrc	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> <. A , l >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )
138	137	fvresd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) = ( +s ` <. A , l >. ) )
139		df-ov	|- ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. )
140		df-ov	|- ( A +s l ) = ( +s ` <. A , l >. )
141	138 139 140	3eqtr4g	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) )
142	114 141	eqtrd	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) )
143	142	eqeq2d	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) )
144	143	ex	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` B ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) )
145	112 144	sylbid	|- ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` ( 2nd ` <. A , B >. ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) )
146	145	imp	|- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) )
147	111 146	rexeqbidva	|- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> E. l e. ( _L ` B ) z = ( A +s l ) ) )
148	147	abbidv	|- ( ( A e. No /\ B e. No ) -> { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } = { z | E. l e. ( _L ` B ) z = ( A +s l ) } )
149	110 148	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) = ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) )
150	69	fveq2d	|- ( ( A e. No /\ B e. No ) -> ( _R ` ( 1st ` <. A , B >. ) ) = ( _R ` A ) )
151	150	eleq2d	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` ( 1st ` <. A , B >. ) ) <-> r e. ( _R ` A ) ) )
152	72	adantr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( 2nd ` <. A , B >. ) = B )
153	152	oveq2d	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) )
154		elun2	|- ( r e. ( _R ` A ) -> r e. ( ( _L ` A ) u. ( _R ` A ) ) )
155		elun1	|- ( r e. ( ( _L ` A ) u. ( _R ` A ) ) -> r e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
156	154 155	syl	|- ( r e. ( _R ` A ) -> r e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
157	156	adantl	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> r e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
158	82	adantr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> B e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
159	157 158	opelxpd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> <. r , B >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) )
160		rightirr	|- ( A e. No -> -. A e. ( _R ` A ) )
161	160	adantr	|- ( ( A e. No /\ B e. No ) -> -. A e. ( _R ` A ) )
162		eleq1	|- ( r = A -> ( r e. ( _R ` A ) <-> A e. ( _R ` A ) ) )
163	162	notbid	|- ( r = A -> ( -. r e. ( _R ` A ) <-> -. A e. ( _R ` A ) ) )
164	161 163	syl5ibrcom	|- ( ( A e. No /\ B e. No ) -> ( r = A -> -. r e. ( _R ` A ) ) )
165	164	necon2ad	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` A ) -> r =/= A ) )
166	165	imp	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> r =/= A )
167	166	orcd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r =/= A \/ B =/= B ) )
168		simpr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> r e. ( _R ` A ) )
169		simplr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> B e. No )
170		opthneg	|- ( ( r e. ( _R ` A ) /\ B e. No ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) )
171	168 169 170	syl2anc	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) )
172	167 171	mpbird	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> <. r , B >. =/= <. A , B >. )
173		eldifsn	|- ( <. r , B >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. r , B >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) /\ <. r , B >. =/= <. A , B >. ) )
174	159 172 173	sylanbrc	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> <. r , B >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )
175	174	fvresd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) = ( +s ` <. r , B >. ) )
176		df-ov	|- ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. )
177		df-ov	|- ( r +s B ) = ( +s ` <. r , B >. )
178	175 176 177	3eqtr4g	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( r +s B ) )
179	153 178	eqtrd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r +s B ) )
180	179	eqeq2d	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) )
181	180	ex	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` A ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) )
182	151 181	sylbid	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` ( 1st ` <. A , B >. ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) )
183	182	imp	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) )
184	150 183	rexeqbidva	|- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _R ` A ) y = ( r +s B ) ) )
185	184	abbidv	|- ( ( A e. No /\ B e. No ) -> { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _R ` A ) y = ( r +s B ) } )
186	72	fveq2d	|- ( ( A e. No /\ B e. No ) -> ( _R ` ( 2nd ` <. A , B >. ) ) = ( _R ` B ) )
187	186	eleq2d	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` ( 2nd ` <. A , B >. ) ) <-> r e. ( _R ` B ) ) )
188	69	adantr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( 1st ` <. A , B >. ) = A )
189	188	oveq1d	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) )
190	116	adantr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> A e. { A } )
191	190 117	syl	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
192		elun2	|- ( r e. ( _R ` B ) -> r e. ( ( _L ` B ) u. ( _R ` B ) ) )
193	192	adantl	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> r e. ( ( _L ` B ) u. ( _R ` B ) ) )
194		elun1	|- ( r e. ( ( _L ` B ) u. ( _R ` B ) ) -> r e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
195	193 194	syl	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> r e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
196	191 195	opelxpd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> <. A , r >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) )
197		rightirr	|- ( B e. No -> -. B e. ( _R ` B ) )
198	197	adantl	|- ( ( A e. No /\ B e. No ) -> -. B e. ( _R ` B ) )
199		eleq1	|- ( r = B -> ( r e. ( _R ` B ) <-> B e. ( _R ` B ) ) )
200	199	notbid	|- ( r = B -> ( -. r e. ( _R ` B ) <-> -. B e. ( _R ` B ) ) )
201	198 200	syl5ibrcom	|- ( ( A e. No /\ B e. No ) -> ( r = B -> -. r e. ( _R ` B ) ) )
202	201	necon2ad	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` B ) -> r =/= B ) )
203	202	imp	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> r =/= B )
204	203	olcd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( A =/= A \/ r =/= B ) )
205		opthneg	|- ( ( A e. No /\ r e. ( _R ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) )
206	205	adantlr	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) )
207	204 206	mpbird	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> <. A , r >. =/= <. A , B >. )
208		eldifsn	|- ( <. A , r >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. A , r >. e. ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) /\ <. A , r >. =/= <. A , B >. ) )
209	196 207 208	sylanbrc	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> <. A , r >. e. ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )
210	209	fvresd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) = ( +s ` <. A , r >. ) )
211		df-ov	|- ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. )
212		df-ov	|- ( A +s r ) = ( +s ` <. A , r >. )
213	210 211 212	3eqtr4g	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) )
214	189 213	eqtrd	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) )
215	214	eqeq2d	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) )
216	215	ex	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` B ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) )
217	187 216	sylbid	|- ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` ( 2nd ` <. A , B >. ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) )
218	217	imp	|- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) )
219	186 218	rexeqbidva	|- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> E. r e. ( _R ` B ) z = ( A +s r ) ) )
220	219	abbidv	|- ( ( A e. No /\ B e. No ) -> { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } = { z | E. r e. ( _R ` B ) z = ( A +s r ) } )
221	185 220	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) = ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) )
222	149 221	oveq12d	|- ( ( A e. No /\ B e. No ) -> ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) )
223	68 222	syl5eq	|- ( ( A e. No /\ B e. No ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) )
224	2 223	eqtrd	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) )