Metamath Proof Explorer

Theorem addsasslem1

Description: Lemma for addition associativity. Expand one form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsasslem.1 
|- ( ph -> A e. No )
addsasslem.2 
|- ( ph -> B e. No )
addsasslem.3 
|- ( ph -> C e. No )
Assertion addsasslem1 
|- ( ph -> ( ( A +s B ) +s C ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsasslem.1 
 |-  ( ph -> A e. No )
2 addsasslem.2 
 |-  ( ph -> B e. No )
3 addsasslem.3 
 |-  ( ph -> C e. No )
4 1 2 addscut 
 |-  ( ph -> ( ( A +s B ) e. No /\ ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
5 4 simp2d 
 |-  ( ph -> ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
6 4 simp3d 
 |-  ( ph -> { ( A +s B ) } <
7 ovex 
 |-  ( A +s B ) e. _V
8 7 snnz 
 |-  { ( A +s B ) } =/= (/)
9 sslttr 
 |-  ( ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
10 8 9 mp3an3 
 |-  ( ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
11 5 6 10 syl2anc 
 |-  ( ph -> ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
12 lltropt 
 |-  ( _Left ` C ) <
13 12 a1i 
 |-  ( ph -> ( _Left ` C ) <
14 addsval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) |s ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) ) )
15 1 2 14 syl2anc 
 |-  ( ph -> ( A +s B ) = ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) |s ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) ) )
16 lrcut 
 |-  ( C e. No -> ( ( _Left ` C ) |s ( _Right ` C ) ) = C )
17 3 16 syl 
 |-  ( ph -> ( ( _Left ` C ) |s ( _Right ` C ) ) = C )
18 17 eqcomd 
 |-  ( ph -> C = ( ( _Left ` C ) |s ( _Right ` C ) ) )
19 11 13 15 18 addsunif 
 |-  ( ph -> ( ( A +s B ) +s C ) = ( ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) )
20 unab 
 |-  ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } ) = { y | ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) }
21 eqeq1 
 |-  ( z = y -> ( z = ( ( A +s m ) +s C ) <-> y = ( ( A +s m ) +s C ) ) )
22 21 rexbidv 
 |-  ( z = y -> ( E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) )
23 22 cbvabv 
 |-  { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } = { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) }
24 23 uneq2i 
 |-  ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } )
25 rexun 
 |-  ( E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) <-> ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) \/ E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) ) )
26 eqeq1 
 |-  ( d = h -> ( d = ( l +s B ) <-> h = ( l +s B ) ) )
27 26 rexbidv 
 |-  ( d = h -> ( E. l e. ( _Left ` A ) d = ( l +s B ) <-> E. l e. ( _Left ` A ) h = ( l +s B ) ) )
28 27 rexab 
 |-  ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) <-> E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) )
29 rexcom4 
 |-  ( E. l e. ( _Left ` A ) E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. h E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) )
30 ovex 
 |-  ( l +s B ) e. _V
31 oveq1 
 |-  ( h = ( l +s B ) -> ( h +s C ) = ( ( l +s B ) +s C ) )
32 31 eqeq2d 
 |-  ( h = ( l +s B ) -> ( y = ( h +s C ) <-> y = ( ( l +s B ) +s C ) ) )
33 30 32 ceqsexv 
 |-  ( E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> y = ( ( l +s B ) +s C ) )
34 33 rexbii 
 |-  ( E. l e. ( _Left ` A ) E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) )
35 r19.41v 
 |-  ( E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) )
36 35 exbii 
 |-  ( E. h E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) )
37 29 34 36 3bitr3ri 
 |-  ( E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) )
38 28 37 bitri 
 |-  ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) )
39 eqeq1 
 |-  ( e = h -> ( e = ( A +s m ) <-> h = ( A +s m ) ) )
40 39 rexbidv 
 |-  ( e = h -> ( E. m e. ( _Left ` B ) e = ( A +s m ) <-> E. m e. ( _Left ` B ) h = ( A +s m ) ) )
41 40 rexab 
 |-  ( E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) <-> E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) )
42 rexcom4 
 |-  ( E. m e. ( _Left ` B ) E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. h E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) )
43 ovex 
 |-  ( A +s m ) e. _V
44 oveq1 
 |-  ( h = ( A +s m ) -> ( h +s C ) = ( ( A +s m ) +s C ) )
45 44 eqeq2d 
 |-  ( h = ( A +s m ) -> ( y = ( h +s C ) <-> y = ( ( A +s m ) +s C ) ) )
46 43 45 ceqsexv 
 |-  ( E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> y = ( ( A +s m ) +s C ) )
47 46 rexbii 
 |-  ( E. m e. ( _Left ` B ) E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) )
48 r19.41v 
 |-  ( E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) )
49 48 exbii 
 |-  ( E. h E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) )
50 42 47 49 3bitr3ri 
 |-  ( E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) )
51 41 50 bitri 
 |-  ( E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) )
52 38 51 orbi12i 
 |-  ( ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) \/ E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) ) <-> ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) )
53 25 52 bitri 
 |-  ( E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) <-> ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) )
54 53 abbii 
 |-  { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } = { y | ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) }
55 20 24 54 3eqtr4ri 
 |-  { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } = ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } )
56 55 uneq1i 
 |-  ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) = ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } )
57 unab 
 |-  ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } ) = { a | ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) }
58 eqeq1 
 |-  ( b = a -> ( b = ( ( A +s q ) +s C ) <-> a = ( ( A +s q ) +s C ) ) )
59 58 rexbidv 
 |-  ( b = a -> ( E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) )
60 59 cbvabv 
 |-  { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } = { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) }
61 60 uneq2i 
 |-  ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) = ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } )
62 rexun 
 |-  ( E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) <-> ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) \/ E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) ) )
63 eqeq1 
 |-  ( f = i -> ( f = ( p +s B ) <-> i = ( p +s B ) ) )
64 63 rexbidv 
 |-  ( f = i -> ( E. p e. ( _Right ` A ) f = ( p +s B ) <-> E. p e. ( _Right ` A ) i = ( p +s B ) ) )
65 64 rexab 
 |-  ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) <-> E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) )
66 rexcom4 
 |-  ( E. p e. ( _Right ` A ) E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. i E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) )
67 ovex 
 |-  ( p +s B ) e. _V
68 oveq1 
 |-  ( i = ( p +s B ) -> ( i +s C ) = ( ( p +s B ) +s C ) )
69 68 eqeq2d 
 |-  ( i = ( p +s B ) -> ( a = ( i +s C ) <-> a = ( ( p +s B ) +s C ) ) )
70 67 69 ceqsexv 
 |-  ( E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> a = ( ( p +s B ) +s C ) )
71 70 rexbii 
 |-  ( E. p e. ( _Right ` A ) E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) )
72 r19.41v 
 |-  ( E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) )
73 72 exbii 
 |-  ( E. i E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) )
74 66 71 73 3bitr3ri 
 |-  ( E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) )
75 65 74 bitri 
 |-  ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) )
76 eqeq1 
 |-  ( g = i -> ( g = ( A +s q ) <-> i = ( A +s q ) ) )
77 76 rexbidv 
 |-  ( g = i -> ( E. q e. ( _Right ` B ) g = ( A +s q ) <-> E. q e. ( _Right ` B ) i = ( A +s q ) ) )
78 77 rexab 
 |-  ( E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) <-> E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) )
79 rexcom4 
 |-  ( E. q e. ( _Right ` B ) E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. i E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) )
80 ovex 
 |-  ( A +s q ) e. _V
81 oveq1 
 |-  ( i = ( A +s q ) -> ( i +s C ) = ( ( A +s q ) +s C ) )
82 81 eqeq2d 
 |-  ( i = ( A +s q ) -> ( a = ( i +s C ) <-> a = ( ( A +s q ) +s C ) ) )
83 80 82 ceqsexv 
 |-  ( E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> a = ( ( A +s q ) +s C ) )
84 83 rexbii 
 |-  ( E. q e. ( _Right ` B ) E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) )
85 r19.41v 
 |-  ( E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) )
86 85 exbii 
 |-  ( E. i E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) )
87 79 84 86 3bitr3ri 
 |-  ( E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) )
88 78 87 bitri 
 |-  ( E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) )
89 75 88 orbi12i 
 |-  ( ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) \/ E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) ) <-> ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) )
90 62 89 bitri 
 |-  ( E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) <-> ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) )
91 90 abbii 
 |-  { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } = { a | ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) }
92 57 61 91 3eqtr4ri 
 |-  { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } = ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } )
93 92 uneq1i 
 |-  ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) = ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } )
94 56 93 oveq12i 
 |-  ( ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) )
95 19 94 eqtrdi 
 |-  ( ph -> ( ( A +s B ) +s C ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) )