Metamath Proof Explorer

Theorem addsdilem1

Description: Lemma for surreal distribution. Expand the left hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses addsdilem.1 
|- ( ph -> A e. No )
addsdilem.2 
|- ( ph -> B e. No )
addsdilem.3 
|- ( ph -> C e. No )
Assertion addsdilem1 
|- ( ph -> ( A x.s ( B +s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 addsdilem.1 
 |-  ( ph -> A e. No )
2 addsdilem.2 
 |-  ( ph -> B e. No )
3 addsdilem.3 
 |-  ( ph -> C e. No )
4 lltropt 
 |-  ( _Left ` A ) <
5 4 a1i 
 |-  ( ph -> ( _Left ` A ) <
6 2 3 addscut2 
 |-  ( ph -> ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) <
7 lrcut 
 |-  ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
8 1 7 syl 
 |-  ( ph -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
9 8 eqcomd 
 |-  ( ph -> A = ( ( _Left ` A ) |s ( _Right ` A ) ) )
10 addsval2 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) = ( ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) |s ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) ) )
11 2 3 10 syl2anc 
 |-  ( ph -> ( B +s C ) = ( ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) |s ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) ) )
12 5 6 9 11 mulsunif 
 |-  ( ph -> ( A x.s ( B +s C ) ) = ( ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) |s ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) ) )
13 unab 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) }
14 r19.43 
 |-  ( E. xL e. ( _Left ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) )
15 rexun 
 |-  ( E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
16 eqeq1 
 |-  ( t = b -> ( t = ( yL +s C ) <-> b = ( yL +s C ) ) )
17 16 rexbidv 
 |-  ( t = b -> ( E. yL e. ( _Left ` B ) t = ( yL +s C ) <-> E. yL e. ( _Left ` B ) b = ( yL +s C ) ) )
18 17 rexab 
 |-  ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
19 rexcom4 
 |-  ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
20 ovex 
 |-  ( yL +s C ) e. _V
21 oveq2 
 |-  ( b = ( yL +s C ) -> ( A x.s b ) = ( A x.s ( yL +s C ) ) )
22 21 oveq2d 
 |-  ( b = ( yL +s C ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) )
23 oveq2 
 |-  ( b = ( yL +s C ) -> ( xL x.s b ) = ( xL x.s ( yL +s C ) ) )
24 22 23 oveq12d 
 |-  ( b = ( yL +s C ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) )
25 24 eqeq2d 
 |-  ( b = ( yL +s C ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) )
26 20 25 ceqsexv 
 |-  ( E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) )
27 26 rexbii 
 |-  ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) )
28 r19.41v 
 |-  ( E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
29 28 exbii 
 |-  ( E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
30 19 27 29 3bitr3ri 
 |-  ( E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) )
31 18 30 bitri 
 |-  ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) )
32 eqeq1 
 |-  ( t = b -> ( t = ( B +s zL ) <-> b = ( B +s zL ) ) )
33 32 rexbidv 
 |-  ( t = b -> ( E. zL e. ( _Left ` C ) t = ( B +s zL ) <-> E. zL e. ( _Left ` C ) b = ( B +s zL ) ) )
34 33 rexab 
 |-  ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
35 rexcom4 
 |-  ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
36 ovex 
 |-  ( B +s zL ) e. _V
37 oveq2 
 |-  ( b = ( B +s zL ) -> ( A x.s b ) = ( A x.s ( B +s zL ) ) )
38 37 oveq2d 
 |-  ( b = ( B +s zL ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) )
39 oveq2 
 |-  ( b = ( B +s zL ) -> ( xL x.s b ) = ( xL x.s ( B +s zL ) ) )
40 38 39 oveq12d 
 |-  ( b = ( B +s zL ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) )
41 40 eqeq2d 
 |-  ( b = ( B +s zL ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) )
42 36 41 ceqsexv 
 |-  ( E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) )
43 42 rexbii 
 |-  ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) )
44 r19.41v 
 |-  ( E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
45 44 exbii 
 |-  ( E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
46 35 43 45 3bitr3ri 
 |-  ( E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) )
47 34 46 bitri 
 |-  ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) )
48 31 47 orbi12i 
 |-  ( ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) )
49 15 48 bitr2i 
 |-  ( ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) )
50 49 rexbii 
 |-  ( E. xL e. ( _Left ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) )
51 14 50 bitr3i 
 |-  ( ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) )
52 51 abbii 
 |-  { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) } = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) }
53 13 52 eqtri 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) }
54 unab 
 |-  ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) = { a | ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) }
55 r19.43 
 |-  ( E. xR e. ( _Right ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) )
56 rexun 
 |-  ( E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
57 eqeq1 
 |-  ( t = b -> ( t = ( yR +s C ) <-> b = ( yR +s C ) ) )
58 57 rexbidv 
 |-  ( t = b -> ( E. yR e. ( _Right ` B ) t = ( yR +s C ) <-> E. yR e. ( _Right ` B ) b = ( yR +s C ) ) )
59 58 rexab 
 |-  ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
60 rexcom4 
 |-  ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
61 ovex 
 |-  ( yR +s C ) e. _V
62 oveq2 
 |-  ( b = ( yR +s C ) -> ( A x.s b ) = ( A x.s ( yR +s C ) ) )
63 62 oveq2d 
 |-  ( b = ( yR +s C ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) )
64 oveq2 
 |-  ( b = ( yR +s C ) -> ( xR x.s b ) = ( xR x.s ( yR +s C ) ) )
65 63 64 oveq12d 
 |-  ( b = ( yR +s C ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) )
66 65 eqeq2d 
 |-  ( b = ( yR +s C ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) )
67 61 66 ceqsexv 
 |-  ( E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) )
68 67 rexbii 
 |-  ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) )
69 r19.41v 
 |-  ( E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
70 69 exbii 
 |-  ( E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
71 60 68 70 3bitr3ri 
 |-  ( E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) )
72 59 71 bitri 
 |-  ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) )
73 eqeq1 
 |-  ( t = b -> ( t = ( B +s zR ) <-> b = ( B +s zR ) ) )
74 73 rexbidv 
 |-  ( t = b -> ( E. zR e. ( _Right ` C ) t = ( B +s zR ) <-> E. zR e. ( _Right ` C ) b = ( B +s zR ) ) )
75 74 rexab 
 |-  ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
76 rexcom4 
 |-  ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
77 ovex 
 |-  ( B +s zR ) e. _V
78 oveq2 
 |-  ( b = ( B +s zR ) -> ( A x.s b ) = ( A x.s ( B +s zR ) ) )
79 78 oveq2d 
 |-  ( b = ( B +s zR ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) )
80 oveq2 
 |-  ( b = ( B +s zR ) -> ( xR x.s b ) = ( xR x.s ( B +s zR ) ) )
81 79 80 oveq12d 
 |-  ( b = ( B +s zR ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) )
82 81 eqeq2d 
 |-  ( b = ( B +s zR ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) )
83 77 82 ceqsexv 
 |-  ( E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) )
84 83 rexbii 
 |-  ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) )
85 r19.41v 
 |-  ( E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
86 85 exbii 
 |-  ( E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
87 76 84 86 3bitr3ri 
 |-  ( E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) )
88 75 87 bitri 
 |-  ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) )
89 72 88 orbi12i 
 |-  ( ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) )
90 56 89 bitr2i 
 |-  ( ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) )
91 90 rexbii 
 |-  ( E. xR e. ( _Right ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) )
92 55 91 bitr3i 
 |-  ( ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) )
93 92 abbii 
 |-  { a | ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) } = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) }
94 54 93 eqtri 
 |-  ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) }
95 53 94 uneq12i 
 |-  ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) = ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } )
96 unab 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) }
97 r19.43 
 |-  ( E. xL e. ( _Left ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) )
98 rexun 
 |-  ( E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
99 58 rexab 
 |-  ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
100 rexcom4 
 |-  ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
101 62 oveq2d 
 |-  ( b = ( yR +s C ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) )
102 oveq2 
 |-  ( b = ( yR +s C ) -> ( xL x.s b ) = ( xL x.s ( yR +s C ) ) )
103 101 102 oveq12d 
 |-  ( b = ( yR +s C ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) )
104 103 eqeq2d 
 |-  ( b = ( yR +s C ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) )
105 61 104 ceqsexv 
 |-  ( E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) )
106 105 rexbii 
 |-  ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) )
107 r19.41v 
 |-  ( E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
108 107 exbii 
 |-  ( E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
109 100 106 108 3bitr3ri 
 |-  ( E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) )
110 99 109 bitri 
 |-  ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) )
111 74 rexab 
 |-  ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
112 rexcom4 
 |-  ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
113 78 oveq2d 
 |-  ( b = ( B +s zR ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) )
114 oveq2 
 |-  ( b = ( B +s zR ) -> ( xL x.s b ) = ( xL x.s ( B +s zR ) ) )
115 113 114 oveq12d 
 |-  ( b = ( B +s zR ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) )
116 115 eqeq2d 
 |-  ( b = ( B +s zR ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) )
117 77 116 ceqsexv 
 |-  ( E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) )
118 117 rexbii 
 |-  ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) )
119 r19.41v 
 |-  ( E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
120 119 exbii 
 |-  ( E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) )
121 112 118 120 3bitr3ri 
 |-  ( E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) )
122 111 121 bitri 
 |-  ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) )
123 110 122 orbi12i 
 |-  ( ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) )
124 98 123 bitr2i 
 |-  ( ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) )
125 124 rexbii 
 |-  ( E. xL e. ( _Left ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) )
126 97 125 bitr3i 
 |-  ( ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) )
127 126 abbii 
 |-  { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) } = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) }
128 96 127 eqtri 
 |-  ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) }
129 unab 
 |-  ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) = { a | ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) }
130 r19.43 
 |-  ( E. xR e. ( _Right ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) )
131 rexun 
 |-  ( E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
132 17 rexab 
 |-  ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
133 rexcom4 
 |-  ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
134 21 oveq2d 
 |-  ( b = ( yL +s C ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) )
135 oveq2 
 |-  ( b = ( yL +s C ) -> ( xR x.s b ) = ( xR x.s ( yL +s C ) ) )
136 134 135 oveq12d 
 |-  ( b = ( yL +s C ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) )
137 136 eqeq2d 
 |-  ( b = ( yL +s C ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) )
138 20 137 ceqsexv 
 |-  ( E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) )
139 138 rexbii 
 |-  ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) )
140 r19.41v 
 |-  ( E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
141 140 exbii 
 |-  ( E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
142 133 139 141 3bitr3ri 
 |-  ( E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) )
143 132 142 bitri 
 |-  ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) )
144 33 rexab 
 |-  ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
145 rexcom4 
 |-  ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
146 37 oveq2d 
 |-  ( b = ( B +s zL ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) )
147 oveq2 
 |-  ( b = ( B +s zL ) -> ( xR x.s b ) = ( xR x.s ( B +s zL ) ) )
148 146 147 oveq12d 
 |-  ( b = ( B +s zL ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) )
149 148 eqeq2d 
 |-  ( b = ( B +s zL ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) )
150 36 149 ceqsexv 
 |-  ( E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) )
151 150 rexbii 
 |-  ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) )
152 r19.41v 
 |-  ( E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
153 152 exbii 
 |-  ( E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) )
154 145 151 153 3bitr3ri 
 |-  ( E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) )
155 144 154 bitri 
 |-  ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) )
156 143 155 orbi12i 
 |-  ( ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) )
157 131 156 bitr2i 
 |-  ( ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) )
158 157 rexbii 
 |-  ( E. xR e. ( _Right ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) )
159 130 158 bitr3i 
 |-  ( ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) )
160 159 abbii 
 |-  { a | ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) } = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) }
161 129 160 eqtri 
 |-  ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) }
162 128 161 uneq12i 
 |-  ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) = ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } )
163 95 162 oveq12i 
 |-  ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) = ( ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) |s ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) )
164 12 163 eqtr4di 
 |-  ( ph -> ( A x.s ( B +s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) )