Metamath Proof Explorer

Theorem addsval

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

Ref Expression
Assertion addsval 
|- ( ( 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. ( _L ` A )
86 85 a1i 
 |-  ( ( 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 71 105 sylbida 
 |-  ( ( ( 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 ) ) )
107 70 106 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 ) ) )
108 107 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 ) } )
109 72 fveq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( _L ` ( 2nd ` <. A , B >. ) ) = ( _L ` B ) )
110 109 eleq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` ( 2nd ` <. A , B >. ) ) <-> l e. ( _L ` B ) ) )
111 69 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( 1st ` <. A , B >. ) = A )
112 111 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 ) )
113 snidg 
 |-  ( A e. No -> A e. { A } )
114 113 adantr 
 |-  ( ( A e. No /\ B e. No ) -> A e. { A } )
115 elun2 
 |-  ( A e. { A } -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
116 114 115 syl 
 |-  ( ( A e. No /\ B e. No ) -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
117 116 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
118 elun1 
 |-  ( l e. ( _L ` B ) -> l e. ( ( _L ` B ) u. ( _R ` B ) ) )
119 elun1 
 |-  ( l e. ( ( _L ` B ) u. ( _R ` B ) ) -> l e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
120 118 119 syl 
 |-  ( l e. ( _L ` B ) -> l e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
121 120 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> l e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
122 117 121 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 } ) ) )
123 leftirr 
 |-  -. B e. ( _L ` B )
124 123 a1i 
 |-  ( ( A e. No /\ B e. No ) -> -. B e. ( _L ` B ) )
125 eleq1 
 |-  ( l = B -> ( l e. ( _L ` B ) <-> B e. ( _L ` B ) ) )
126 125 notbid 
 |-  ( l = B -> ( -. l e. ( _L ` B ) <-> -. B e. ( _L ` B ) ) )
127 124 126 syl5ibrcom 
 |-  ( ( A e. No /\ B e. No ) -> ( l = B -> -. l e. ( _L ` B ) ) )
128 127 necon2ad 
 |-  ( ( A e. No /\ B e. No ) -> ( l e. ( _L ` B ) -> l =/= B ) )
129 128 imp 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> l =/= B )
130 129 olcd 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( A =/= A \/ l =/= B ) )
131 opthneg 
 |-  ( ( A e. No /\ l e. ( _L ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) )
132 131 adantlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) )
133 130 132 mpbird 
 |-  ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> <. A , l >. =/= <. A , B >. )
134 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 >. ) )
135 122 133 134 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 >. } ) )
136 135 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 >. ) )
137 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 >. )
138 df-ov 
 |-  ( A +s l ) = ( +s ` <. A , l >. )
139 136 137 138 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 ) )
140 112 139 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 ) )
141 140 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 ) ) )
142 110 141 sylbida 
 |-  ( ( ( 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 ) ) )
143 109 142 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 ) ) )
144 143 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 ) } )
145 108 144 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 ) } ) )
146 69 fveq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( _R ` ( 1st ` <. A , B >. ) ) = ( _R ` A ) )
147 146 eleq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` ( 1st ` <. A , B >. ) ) <-> r e. ( _R ` A ) ) )
148 72 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( 2nd ` <. A , B >. ) = B )
149 148 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 ) )
150 elun2 
 |-  ( r e. ( _R ` A ) -> r e. ( ( _L ` A ) u. ( _R ` A ) ) )
151 elun1 
 |-  ( r e. ( ( _L ` A ) u. ( _R ` A ) ) -> r e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
152 150 151 syl 
 |-  ( r e. ( _R ` A ) -> r e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
153 152 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> r e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
154 82 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> B e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
155 153 154 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 } ) ) )
156 rightirr 
 |-  -. A e. ( _R ` A )
157 156 a1i 
 |-  ( ( A e. No /\ B e. No ) -> -. A e. ( _R ` A ) )
158 eleq1 
 |-  ( r = A -> ( r e. ( _R ` A ) <-> A e. ( _R ` A ) ) )
159 158 notbid 
 |-  ( r = A -> ( -. r e. ( _R ` A ) <-> -. A e. ( _R ` A ) ) )
160 157 159 syl5ibrcom 
 |-  ( ( A e. No /\ B e. No ) -> ( r = A -> -. r e. ( _R ` A ) ) )
161 160 necon2ad 
 |-  ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` A ) -> r =/= A ) )
162 161 imp 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> r =/= A )
163 162 orcd 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r =/= A \/ B =/= B ) )
164 simpr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> r e. ( _R ` A ) )
165 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> B e. No )
166 opthneg 
 |-  ( ( r e. ( _R ` A ) /\ B e. No ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) )
167 164 165 166 syl2anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) )
168 163 167 mpbird 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> <. r , B >. =/= <. A , B >. )
169 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 >. ) )
170 155 168 169 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 >. } ) )
171 170 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 >. ) )
172 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 >. )
173 df-ov 
 |-  ( r +s B ) = ( +s ` <. r , B >. )
174 171 172 173 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 ) )
175 149 174 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 ) )
176 175 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 ) ) )
177 147 176 sylbida 
 |-  ( ( ( 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 ) ) )
178 146 177 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 ) ) )
179 178 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 ) } )
180 72 fveq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( _R ` ( 2nd ` <. A , B >. ) ) = ( _R ` B ) )
181 180 eleq2d 
 |-  ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` ( 2nd ` <. A , B >. ) ) <-> r e. ( _R ` B ) ) )
182 69 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( 1st ` <. A , B >. ) = A )
183 182 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 ) )
184 114 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> A e. { A } )
185 184 115 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> A e. ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
186 elun2 
 |-  ( r e. ( _R ` B ) -> r e. ( ( _L ` B ) u. ( _R ` B ) ) )
187 186 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> r e. ( ( _L ` B ) u. ( _R ` B ) ) )
188 elun1 
 |-  ( r e. ( ( _L ` B ) u. ( _R ` B ) ) -> r e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
189 187 188 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> r e. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
190 185 189 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 } ) ) )
191 rightirr 
 |-  -. B e. ( _R ` B )
192 191 a1i 
 |-  ( ( A e. No /\ B e. No ) -> -. B e. ( _R ` B ) )
193 eleq1 
 |-  ( r = B -> ( r e. ( _R ` B ) <-> B e. ( _R ` B ) ) )
194 193 notbid 
 |-  ( r = B -> ( -. r e. ( _R ` B ) <-> -. B e. ( _R ` B ) ) )
195 192 194 syl5ibrcom 
 |-  ( ( A e. No /\ B e. No ) -> ( r = B -> -. r e. ( _R ` B ) ) )
196 195 necon2ad 
 |-  ( ( A e. No /\ B e. No ) -> ( r e. ( _R ` B ) -> r =/= B ) )
197 196 imp 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> r =/= B )
198 197 olcd 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( A =/= A \/ r =/= B ) )
199 opthneg 
 |-  ( ( A e. No /\ r e. ( _R ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) )
200 199 adantlr 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) )
201 198 200 mpbird 
 |-  ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> <. A , r >. =/= <. A , B >. )
202 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 >. ) )
203 190 201 202 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 >. } ) )
204 203 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 >. ) )
205 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 >. )
206 df-ov 
 |-  ( A +s r ) = ( +s ` <. A , r >. )
207 204 205 206 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 ) )
208 183 207 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 ) )
209 208 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 ) ) )
210 181 209 sylbida 
 |-  ( ( ( 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 ) ) )
211 180 210 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 ) ) )
212 211 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 ) } )
213 179 212 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 ) } ) )
214 145 213 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 ) } ) ) )
215 68 214 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 ) } ) ) )
216 2 215 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 ) } ) ) )