Metamath Proof Explorer

Theorem mulsuniflem

Description: Lemma for mulsunif . State the theorem with some extra distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses mulsuniflem.1 
|- ( ph -> L <
mulsuniflem.2 
|- ( ph -> M <
mulsuniflem.3 
|- ( ph -> A = ( L |s R ) )
mulsuniflem.4 
|- ( ph -> B = ( M |s S ) )
Assertion mulsuniflem 
|- ( ph -> ( A x.s B ) = ( ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 mulsuniflem.1 
 |-  ( ph -> L <
2 mulsuniflem.2 
 |-  ( ph -> M <
3 mulsuniflem.3 
 |-  ( ph -> A = ( L |s R ) )
4 mulsuniflem.4 
 |-  ( ph -> B = ( M |s S ) )
5 1 scutcld 
 |-  ( ph -> ( L |s R ) e. No )
6 3 5 eqeltrd 
 |-  ( ph -> A e. No )
7 2 scutcld 
 |-  ( ph -> ( M |s S ) e. No )
8 4 7 eqeltrd 
 |-  ( ph -> B e. No )
9 mulsval 
 |-  ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) |s ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) ) )
10 6 8 9 syl2anc 
 |-  ( ph -> ( A x.s B ) = ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) |s ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) ) )
11 6 8 mulscut2 
 |-  ( ph -> ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) <
12 1 3 cofcutr1d 
 |-  ( ph -> A. f e. ( _Left ` A ) E. p e. L f <_s p )
13 2 4 cofcutr1d 
 |-  ( ph -> A. g e. ( _Left ` B ) E. q e. M g <_s q )
14 13 adantr 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) ) -> A. g e. ( _Left ` B ) E. q e. M g <_s q )
15 reeanv 
 |-  ( E. p e. L E. q e. M ( f <_s p /\ g <_s q ) <-> ( E. p e. L f <_s p /\ E. q e. M g <_s q ) )
16 leftssno 
 |-  ( _Left ` A ) C_ No
17 simprl 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> f e. ( _Left ` A ) )
18 16 17 sselid 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> f e. No )
19 18 adantrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> f e. No )
20 8 adantr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> B e. No )
21 19 20 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( f x.s B ) e. No )
22 6 adantr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> A e. No )
23 leftssno 
 |-  ( _Left ` B ) C_ No
24 simprr 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> g e. ( _Left ` B ) )
25 23 24 sselid 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> g e. No )
26 25 adantrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> g e. No )
27 22 26 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( A x.s g ) e. No )
28 21 27 addscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( f x.s B ) +s ( A x.s g ) ) e. No )
29 19 26 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( f x.s g ) e. No )
30 28 29 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) e. No )
31 30 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) e. No )
32 ssltss1 
 |-  ( L < L C_ No )
33 1 32 syl 
 |-  ( ph -> L C_ No )
34 33 adantr 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> L C_ No )
35 simprl 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> p e. L )
36 34 35 sseldd 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> p e. No )
37 36 adantrl 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> p e. No )
38 37 20 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( p x.s B ) e. No )
39 38 27 addscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( p x.s B ) +s ( A x.s g ) ) e. No )
40 37 26 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( p x.s g ) e. No )
41 39 40 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) e. No )
42 41 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) e. No )
43 ssltss1 
 |-  ( M < M C_ No )
44 2 43 syl 
 |-  ( ph -> M C_ No )
45 44 adantr 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> M C_ No )
46 simprr 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> q e. M )
47 45 46 sseldd 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> q e. No )
48 47 adantrl 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> q e. No )
49 22 48 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( A x.s q ) e. No )
50 38 49 addscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( p x.s B ) +s ( A x.s q ) ) e. No )
51 37 48 mulscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( p x.s q ) e. No )
52 50 51 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No )
53 52 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No )
54 18 adantrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> f e. No )
55 37 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> p e. No )
56 25 adantrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> g e. No )
57 8 adantr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> B e. No )
58 simprrl 
 |-  ( ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) -> f <_s p )
59 58 adantl 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> f <_s p )
60 8 adantr 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> B e. No )
61 ssltleft 
 |-  ( B e. No -> ( _Left ` B ) <
62 8 61 syl 
 |-  ( ph -> ( _Left ` B ) <
63 62 adantr 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> ( _Left ` B ) <
64 snidg 
 |-  ( B e. No -> B e. { B } )
65 8 64 syl 
 |-  ( ph -> B e. { B } )
66 65 adantr 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> B e. { B } )
67 63 24 66 ssltsepcd 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> g
68 25 60 67 sltled 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> g <_s B )
69 68 adantrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> g <_s B )
70 54 55 56 57 59 69 slemuld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( f x.s B ) -s ( f x.s g ) ) <_s ( ( p x.s B ) -s ( p x.s g ) ) )
71 21 29 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( f x.s B ) -s ( f x.s g ) ) e. No )
72 38 40 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( p x.s B ) -s ( p x.s g ) ) e. No )
73 71 72 27 sleadd1d 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( f x.s B ) -s ( f x.s g ) ) <_s ( ( p x.s B ) -s ( p x.s g ) ) <-> ( ( ( f x.s B ) -s ( f x.s g ) ) +s ( A x.s g ) ) <_s ( ( ( p x.s B ) -s ( p x.s g ) ) +s ( A x.s g ) ) ) )
74 73 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( f x.s B ) -s ( f x.s g ) ) <_s ( ( p x.s B ) -s ( p x.s g ) ) <-> ( ( ( f x.s B ) -s ( f x.s g ) ) +s ( A x.s g ) ) <_s ( ( ( p x.s B ) -s ( p x.s g ) ) +s ( A x.s g ) ) ) )
75 70 74 mpbid 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( f x.s B ) -s ( f x.s g ) ) +s ( A x.s g ) ) <_s ( ( ( p x.s B ) -s ( p x.s g ) ) +s ( A x.s g ) ) )
76 21 27 29 addsubsd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) = ( ( ( f x.s B ) -s ( f x.s g ) ) +s ( A x.s g ) ) )
77 76 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) = ( ( ( f x.s B ) -s ( f x.s g ) ) +s ( A x.s g ) ) )
78 38 27 40 addsubsd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) = ( ( ( p x.s B ) -s ( p x.s g ) ) +s ( A x.s g ) ) )
79 78 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) = ( ( ( p x.s B ) -s ( p x.s g ) ) +s ( A x.s g ) ) )
80 75 77 79 3brtr4d 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) )
81 6 adantr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> A e. No )
82 48 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> q e. No )
83 6 adantr 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> A e. No )
84 scutcut 
 |-  ( L < ( ( L |s R ) e. No /\ L <
85 1 84 syl 
 |-  ( ph -> ( ( L |s R ) e. No /\ L <
86 85 simp2d 
 |-  ( ph -> L <
87 86 adantr 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> L <
88 ovex 
 |-  ( L |s R ) e. _V
89 88 snid 
 |-  ( L |s R ) e. { ( L |s R ) }
90 3 89 eqeltrdi 
 |-  ( ph -> A e. { ( L |s R ) } )
91 90 adantr 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> A e. { ( L |s R ) } )
92 87 35 91 ssltsepcd 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> p
93 36 83 92 sltled 
 |-  ( ( ph /\ ( p e. L /\ q e. M ) ) -> p <_s A )
94 93 adantrl 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> p <_s A )
95 94 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> p <_s A )
96 simprrr 
 |-  ( ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) -> g <_s q )
97 96 adantl 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> g <_s q )
98 55 81 56 82 95 97 slemuld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( p x.s q ) -s ( p x.s g ) ) <_s ( ( A x.s q ) -s ( A x.s g ) ) )
99 51 49 40 27 slesubsub3bd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s q ) -s ( p x.s g ) ) <_s ( ( A x.s q ) -s ( A x.s g ) ) <-> ( ( A x.s g ) -s ( p x.s g ) ) <_s ( ( A x.s q ) -s ( p x.s q ) ) ) )
100 27 40 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( A x.s g ) -s ( p x.s g ) ) e. No )
101 49 51 subscld 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( A x.s q ) -s ( p x.s q ) ) e. No )
102 100 101 38 sleadd2d 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( A x.s g ) -s ( p x.s g ) ) <_s ( ( A x.s q ) -s ( p x.s q ) ) <-> ( ( p x.s B ) +s ( ( A x.s g ) -s ( p x.s g ) ) ) <_s ( ( p x.s B ) +s ( ( A x.s q ) -s ( p x.s q ) ) ) ) )
103 99 102 bitrd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s q ) -s ( p x.s g ) ) <_s ( ( A x.s q ) -s ( A x.s g ) ) <-> ( ( p x.s B ) +s ( ( A x.s g ) -s ( p x.s g ) ) ) <_s ( ( p x.s B ) +s ( ( A x.s q ) -s ( p x.s q ) ) ) ) )
104 103 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s q ) -s ( p x.s g ) ) <_s ( ( A x.s q ) -s ( A x.s g ) ) <-> ( ( p x.s B ) +s ( ( A x.s g ) -s ( p x.s g ) ) ) <_s ( ( p x.s B ) +s ( ( A x.s q ) -s ( p x.s q ) ) ) ) )
105 98 104 mpbid 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( p x.s B ) +s ( ( A x.s g ) -s ( p x.s g ) ) ) <_s ( ( p x.s B ) +s ( ( A x.s q ) -s ( p x.s q ) ) ) )
106 38 27 40 addsubsassd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) = ( ( p x.s B ) +s ( ( A x.s g ) -s ( p x.s g ) ) ) )
107 106 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) = ( ( p x.s B ) +s ( ( A x.s g ) -s ( p x.s g ) ) ) )
108 38 49 51 addsubsassd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( p e. L /\ q e. M ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) = ( ( p x.s B ) +s ( ( A x.s q ) -s ( p x.s q ) ) ) )
109 108 adantrrr 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) = ( ( p x.s B ) +s ( ( A x.s q ) -s ( p x.s q ) ) ) )
110 105 107 109 3brtr4d 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s g ) ) -s ( p x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
111 31 42 53 80 110 sletrd 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
112 111 anassrs 
 |-  ( ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) /\ ( ( p e. L /\ q e. M ) /\ ( f <_s p /\ g <_s q ) ) ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
113 112 expr 
 |-  ( ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) /\ ( p e. L /\ q e. M ) ) -> ( ( f <_s p /\ g <_s q ) -> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
114 113 reximdvva 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) ) -> ( E. p e. L E. q e. M ( f <_s p /\ g <_s q ) -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
115 114 expcom 
 |-  ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) -> ( ph -> ( E. p e. L E. q e. M ( f <_s p /\ g <_s q ) -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) ) )
116 115 com23 
 |-  ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) -> ( E. p e. L E. q e. M ( f <_s p /\ g <_s q ) -> ( ph -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) ) )
117 116 imp 
 |-  ( ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ E. p e. L E. q e. M ( f <_s p /\ g <_s q ) ) -> ( ph -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
118 15 117 sylan2br 
 |-  ( ( ( f e. ( _Left ` A ) /\ g e. ( _Left ` B ) ) /\ ( E. p e. L f <_s p /\ E. q e. M g <_s q ) ) -> ( ph -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
119 118 an4s 
 |-  ( ( ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) /\ ( g e. ( _Left ` B ) /\ E. q e. M g <_s q ) ) -> ( ph -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
120 119 impcom 
 |-  ( ( ph /\ ( ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) /\ ( g e. ( _Left ` B ) /\ E. q e. M g <_s q ) ) ) -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
121 120 anassrs 
 |-  ( ( ( ph /\ ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) ) /\ ( g e. ( _Left ` B ) /\ E. q e. M g <_s q ) ) -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
122 121 expr 
 |-  ( ( ( ph /\ ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) ) /\ g e. ( _Left ` B ) ) -> ( E. q e. M g <_s q -> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
123 122 ralimdva 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) ) -> ( A. g e. ( _Left ` B ) E. q e. M g <_s q -> A. g e. ( _Left ` B ) E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
124 14 123 mpd 
 |-  ( ( ph /\ ( f e. ( _Left ` A ) /\ E. p e. L f <_s p ) ) -> A. g e. ( _Left ` B ) E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
125 124 expr 
 |-  ( ( ph /\ f e. ( _Left ` A ) ) -> ( E. p e. L f <_s p -> A. g e. ( _Left ` B ) E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
126 125 ralimdva 
 |-  ( ph -> ( A. f e. ( _Left ` A ) E. p e. L f <_s p -> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
127 12 126 mpd 
 |-  ( ph -> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
128 eqeq1 
 |-  ( a = z -> ( a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
129 128 2rexbidv 
 |-  ( a = z -> ( E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. p e. L E. q e. M z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
130 129 rexab 
 |-  ( E. z e. { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z <-> E. z ( E. p e. L E. q e. M z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
131 r19.41vv 
 |-  ( E. p e. L E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> ( E. p e. L E. q e. M z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
132 131 exbii 
 |-  ( E. z E. p e. L E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. z ( E. p e. L E. q e. M z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
133 rexcom4 
 |-  ( E. p e. L E. z E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. z E. p e. L E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
134 rexcom4 
 |-  ( E. q e. M E. z ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. z E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
135 ovex 
 |-  ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. _V
136 breq2 
 |-  ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
137 135 136 ceqsexv 
 |-  ( E. z ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
138 137 rexbii 
 |-  ( E. q e. M E. z ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
139 134 138 bitr3i 
 |-  ( E. z E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
140 139 rexbii 
 |-  ( E. p e. L E. z E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
141 133 140 bitr3i 
 |-  ( E. z E. p e. L E. q e. M ( z = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) <-> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
142 130 132 141 3bitr2i 
 |-  ( E. z e. { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z <-> E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
143 ssun1 
 |-  { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } C_ ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } )
144 ssrexv 
 |-  ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } C_ ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) -> ( E. z e. { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
145 143 144 ax-mp 
 |-  ( E. z e. { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
146 142 145 sylbir 
 |-  ( E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
147 146 2ralimi 
 |-  ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. p e. L E. q e. M ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
148 127 147 syl 
 |-  ( ph -> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
149 1 3 cofcutr2d 
 |-  ( ph -> A. i e. ( _Right ` A ) E. r e. R r <_s i )
150 2 4 cofcutr2d 
 |-  ( ph -> A. j e. ( _Right ` B ) E. s e. S s <_s j )
151 150 adantr 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) ) -> A. j e. ( _Right ` B ) E. s e. S s <_s j )
152 reeanv 
 |-  ( E. r e. R E. s e. S ( r <_s i /\ s <_s j ) <-> ( E. r e. R r <_s i /\ E. s e. S s <_s j ) )
153 rightssno 
 |-  ( _Right ` A ) C_ No
154 simprl 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> i e. ( _Right ` A ) )
155 153 154 sselid 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> i e. No )
156 155 adantrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> i e. No )
157 8 adantr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> B e. No )
158 156 157 mulscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( i x.s B ) e. No )
159 6 adantr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> A e. No )
160 rightssno 
 |-  ( _Right ` B ) C_ No
161 simprr 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> j e. ( _Right ` B ) )
162 160 161 sselid 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> j e. No )
163 162 adantrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> j e. No )
164 159 163 mulscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( A x.s j ) e. No )
165 158 164 addscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( i x.s B ) +s ( A x.s j ) ) e. No )
166 156 163 mulscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( i x.s j ) e. No )
167 165 166 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) e. No )
168 167 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) e. No )
169 ssltss2 
 |-  ( L < R C_ No )
170 1 169 syl 
 |-  ( ph -> R C_ No )
171 170 adantr 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> R C_ No )
172 simprl 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> r e. R )
173 171 172 sseldd 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> r e. No )
174 173 adantrl 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> r e. No )
175 174 157 mulscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( r x.s B ) e. No )
176 175 164 addscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( r x.s B ) +s ( A x.s j ) ) e. No )
177 174 163 mulscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( r x.s j ) e. No )
178 176 177 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) e. No )
179 178 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) e. No )
180 ssltss2 
 |-  ( M < S C_ No )
181 2 180 syl 
 |-  ( ph -> S C_ No )
182 181 adantr 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> S C_ No )
183 simprr 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> s e. S )
184 182 183 sseldd 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> s e. No )
185 184 adantrl 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> s e. No )
186 159 185 mulscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( A x.s s ) e. No )
187 175 186 addscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( r x.s B ) +s ( A x.s s ) ) e. No )
188 173 184 mulscld 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> ( r x.s s ) e. No )
189 188 adantrl 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( r x.s s ) e. No )
190 187 189 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No )
191 190 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No )
192 174 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> r e. No )
193 155 adantrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> i e. No )
194 8 adantr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> B e. No )
195 162 adantrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> j e. No )
196 simprrl 
 |-  ( ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) -> r <_s i )
197 196 adantl 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> r <_s i )
198 8 adantr 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> B e. No )
199 ssltright 
 |-  ( B e. No -> { B } <
200 8 199 syl 
 |-  ( ph -> { B } <
201 200 adantr 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> { B } <
202 65 adantr 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> B e. { B } )
203 201 202 161 ssltsepcd 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> B
204 198 162 203 sltled 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> B <_s j )
205 204 adantrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> B <_s j )
206 192 193 194 195 197 205 slemuld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( r x.s j ) -s ( r x.s B ) ) <_s ( ( i x.s j ) -s ( i x.s B ) ) )
207 177 175 166 158 slesubsub2bd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s j ) -s ( r x.s B ) ) <_s ( ( i x.s j ) -s ( i x.s B ) ) <-> ( ( i x.s B ) -s ( i x.s j ) ) <_s ( ( r x.s B ) -s ( r x.s j ) ) ) )
208 158 166 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( i x.s B ) -s ( i x.s j ) ) e. No )
209 175 177 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( r x.s B ) -s ( r x.s j ) ) e. No )
210 208 209 164 sleadd1d 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( i x.s B ) -s ( i x.s j ) ) <_s ( ( r x.s B ) -s ( r x.s j ) ) <-> ( ( ( i x.s B ) -s ( i x.s j ) ) +s ( A x.s j ) ) <_s ( ( ( r x.s B ) -s ( r x.s j ) ) +s ( A x.s j ) ) ) )
211 207 210 bitrd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s j ) -s ( r x.s B ) ) <_s ( ( i x.s j ) -s ( i x.s B ) ) <-> ( ( ( i x.s B ) -s ( i x.s j ) ) +s ( A x.s j ) ) <_s ( ( ( r x.s B ) -s ( r x.s j ) ) +s ( A x.s j ) ) ) )
212 211 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s j ) -s ( r x.s B ) ) <_s ( ( i x.s j ) -s ( i x.s B ) ) <-> ( ( ( i x.s B ) -s ( i x.s j ) ) +s ( A x.s j ) ) <_s ( ( ( r x.s B ) -s ( r x.s j ) ) +s ( A x.s j ) ) ) )
213 206 212 mpbid 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( i x.s B ) -s ( i x.s j ) ) +s ( A x.s j ) ) <_s ( ( ( r x.s B ) -s ( r x.s j ) ) +s ( A x.s j ) ) )
214 158 164 166 addsubsd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) = ( ( ( i x.s B ) -s ( i x.s j ) ) +s ( A x.s j ) ) )
215 214 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) = ( ( ( i x.s B ) -s ( i x.s j ) ) +s ( A x.s j ) ) )
216 175 164 177 addsubsd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) = ( ( ( r x.s B ) -s ( r x.s j ) ) +s ( A x.s j ) ) )
217 216 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) = ( ( ( r x.s B ) -s ( r x.s j ) ) +s ( A x.s j ) ) )
218 213 215 217 3brtr4d 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) )
219 6 adantr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> A e. No )
220 185 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> s e. No )
221 6 adantr 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> A e. No )
222 85 simp3d 
 |-  ( ph -> { ( L |s R ) } <
223 222 adantr 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> { ( L |s R ) } <
224 90 adantr 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> A e. { ( L |s R ) } )
225 223 224 172 ssltsepcd 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> A
226 221 173 225 sltled 
 |-  ( ( ph /\ ( r e. R /\ s e. S ) ) -> A <_s r )
227 226 adantrl 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> A <_s r )
228 227 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> A <_s r )
229 simprrr 
 |-  ( ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) -> s <_s j )
230 229 adantl 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> s <_s j )
231 219 192 220 195 228 230 slemuld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( A x.s j ) -s ( A x.s s ) ) <_s ( ( r x.s j ) -s ( r x.s s ) ) )
232 164 177 186 189 slesubsubbd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( A x.s j ) -s ( A x.s s ) ) <_s ( ( r x.s j ) -s ( r x.s s ) ) <-> ( ( A x.s j ) -s ( r x.s j ) ) <_s ( ( A x.s s ) -s ( r x.s s ) ) ) )
233 164 177 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( A x.s j ) -s ( r x.s j ) ) e. No )
234 186 189 subscld 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( A x.s s ) -s ( r x.s s ) ) e. No )
235 233 234 175 sleadd2d 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( A x.s j ) -s ( r x.s j ) ) <_s ( ( A x.s s ) -s ( r x.s s ) ) <-> ( ( r x.s B ) +s ( ( A x.s j ) -s ( r x.s j ) ) ) <_s ( ( r x.s B ) +s ( ( A x.s s ) -s ( r x.s s ) ) ) ) )
236 232 235 bitrd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( A x.s j ) -s ( A x.s s ) ) <_s ( ( r x.s j ) -s ( r x.s s ) ) <-> ( ( r x.s B ) +s ( ( A x.s j ) -s ( r x.s j ) ) ) <_s ( ( r x.s B ) +s ( ( A x.s s ) -s ( r x.s s ) ) ) ) )
237 236 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( A x.s j ) -s ( A x.s s ) ) <_s ( ( r x.s j ) -s ( r x.s s ) ) <-> ( ( r x.s B ) +s ( ( A x.s j ) -s ( r x.s j ) ) ) <_s ( ( r x.s B ) +s ( ( A x.s s ) -s ( r x.s s ) ) ) ) )
238 231 237 mpbid 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( r x.s B ) +s ( ( A x.s j ) -s ( r x.s j ) ) ) <_s ( ( r x.s B ) +s ( ( A x.s s ) -s ( r x.s s ) ) ) )
239 175 164 177 addsubsassd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) = ( ( r x.s B ) +s ( ( A x.s j ) -s ( r x.s j ) ) ) )
240 239 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) = ( ( r x.s B ) +s ( ( A x.s j ) -s ( r x.s j ) ) ) )
241 175 186 189 addsubsassd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( r e. R /\ s e. S ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) = ( ( r x.s B ) +s ( ( A x.s s ) -s ( r x.s s ) ) ) )
242 241 adantrrr 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) = ( ( r x.s B ) +s ( ( A x.s s ) -s ( r x.s s ) ) ) )
243 238 240 242 3brtr4d 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s j ) ) -s ( r x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
244 168 179 191 218 243 sletrd 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
245 244 anassrs 
 |-  ( ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) /\ ( ( r e. R /\ s e. S ) /\ ( r <_s i /\ s <_s j ) ) ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
246 245 expr 
 |-  ( ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( r <_s i /\ s <_s j ) -> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
247 246 reximdvva 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) ) -> ( E. r e. R E. s e. S ( r <_s i /\ s <_s j ) -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
248 247 expcom 
 |-  ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) -> ( ph -> ( E. r e. R E. s e. S ( r <_s i /\ s <_s j ) -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) )
249 248 com23 
 |-  ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) -> ( E. r e. R E. s e. S ( r <_s i /\ s <_s j ) -> ( ph -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) ) )
250 249 imp 
 |-  ( ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ E. r e. R E. s e. S ( r <_s i /\ s <_s j ) ) -> ( ph -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
251 152 250 sylan2br 
 |-  ( ( ( i e. ( _Right ` A ) /\ j e. ( _Right ` B ) ) /\ ( E. r e. R r <_s i /\ E. s e. S s <_s j ) ) -> ( ph -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
252 251 an4s 
 |-  ( ( ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) /\ ( j e. ( _Right ` B ) /\ E. s e. S s <_s j ) ) -> ( ph -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
253 252 impcom 
 |-  ( ( ph /\ ( ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) /\ ( j e. ( _Right ` B ) /\ E. s e. S s <_s j ) ) ) -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
254 253 anassrs 
 |-  ( ( ( ph /\ ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) ) /\ ( j e. ( _Right ` B ) /\ E. s e. S s <_s j ) ) -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
255 254 expr 
 |-  ( ( ( ph /\ ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) ) /\ j e. ( _Right ` B ) ) -> ( E. s e. S s <_s j -> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
256 255 ralimdva 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) ) -> ( A. j e. ( _Right ` B ) E. s e. S s <_s j -> A. j e. ( _Right ` B ) E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
257 151 256 mpd 
 |-  ( ( ph /\ ( i e. ( _Right ` A ) /\ E. r e. R r <_s i ) ) -> A. j e. ( _Right ` B ) E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
258 257 expr 
 |-  ( ( ph /\ i e. ( _Right ` A ) ) -> ( E. r e. R r <_s i -> A. j e. ( _Right ` B ) E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
259 258 ralimdva 
 |-  ( ph -> ( A. i e. ( _Right ` A ) E. r e. R r <_s i -> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
260 149 259 mpd 
 |-  ( ph -> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
261 eqeq1 
 |-  ( b = z -> ( b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
262 261 2rexbidv 
 |-  ( b = z -> ( E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> E. r e. R E. s e. S z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
263 262 rexab 
 |-  ( E. z e. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z <-> E. z ( E. r e. R E. s e. S z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
264 r19.41vv 
 |-  ( E. r e. R E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> ( E. r e. R E. s e. S z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
265 264 exbii 
 |-  ( E. z E. r e. R E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. z ( E. r e. R E. s e. S z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
266 rexcom4 
 |-  ( E. r e. R E. z E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. z E. r e. R E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
267 rexcom4 
 |-  ( E. s e. S E. z ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. z E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
268 ovex 
 |-  ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. _V
269 breq2 
 |-  ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
270 268 269 ceqsexv 
 |-  ( E. z ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
271 270 rexbii 
 |-  ( E. s e. S E. z ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
272 267 271 bitr3i 
 |-  ( E. z E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
273 272 rexbii 
 |-  ( E. r e. R E. z E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
274 266 273 bitr3i 
 |-  ( E. z E. r e. R E. s e. S ( z = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) <-> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
275 263 265 274 3bitr2i 
 |-  ( E. z e. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z <-> E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
276 ssun2 
 |-  { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } C_ ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } )
277 ssrexv 
 |-  ( { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } C_ ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) -> ( E. z e. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
278 276 277 ax-mp 
 |-  ( E. z e. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
279 275 278 sylbir 
 |-  ( E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
280 279 2ralimi 
 |-  ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. r e. R E. s e. S ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
281 260 280 syl 
 |-  ( ph -> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
282 ralunb 
 |-  ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
283 eqeq1 
 |-  ( e = xO -> ( e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) )
284 283 2rexbidv 
 |-  ( e = xO -> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) )
285 284 ralab 
 |-  ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
286 r19.23v 
 |-  ( A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
287 286 ralbii 
 |-  ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
288 r19.23v 
 |-  ( A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
289 287 288 bitri 
 |-  ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
290 289 albii 
 |-  ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
291 ralcom4 
 |-  ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
292 ralcom4 
 |-  ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
293 ovex 
 |-  ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) e. _V
294 breq1 
 |-  ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( xO <_s z <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
295 294 rexbidv 
 |-  ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) )
296 293 295 ceqsalv 
 |-  ( A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
297 296 ralbii 
 |-  ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
298 292 297 bitr3i 
 |-  ( A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
299 298 ralbii 
 |-  ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
300 291 299 bitr3i 
 |-  ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
301 285 290 300 3bitr2i 
 |-  ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z )
302 eqeq1 
 |-  ( h = xO -> ( h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) )
303 302 2rexbidv 
 |-  ( h = xO -> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) )
304 303 ralab 
 |-  ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
305 r19.23v 
 |-  ( A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
306 305 ralbii 
 |-  ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
307 r19.23v 
 |-  ( A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
308 306 307 bitri 
 |-  ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
309 308 albii 
 |-  ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
310 ralcom4 
 |-  ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
311 ralcom4 
 |-  ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) )
312 ovex 
 |-  ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) e. _V
313 breq1 
 |-  ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( xO <_s z <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
314 313 rexbidv 
 |-  ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
315 312 314 ceqsalv 
 |-  ( A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
316 315 ralbii 
 |-  ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
317 311 316 bitr3i 
 |-  ( A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
318 317 ralbii 
 |-  ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
319 310 318 bitr3i 
 |-  ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
320 304 309 319 3bitr2i 
 |-  ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z )
321 301 320 anbi12i 
 |-  ( ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
322 282 321 bitri 
 |-  ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) )
323 148 281 322 sylanbrc 
 |-  ( ph -> A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z )
324 1 3 cofcutr1d 
 |-  ( ph -> A. l e. ( _Left ` A ) E. t e. L l <_s t )
325 2 4 cofcutr2d 
 |-  ( ph -> A. m e. ( _Right ` B ) E. u e. S u <_s m )
326 325 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) ) -> A. m e. ( _Right ` B ) E. u e. S u <_s m )
327 reeanv 
 |-  ( E. t e. L E. u e. S ( l <_s t /\ u <_s m ) <-> ( E. t e. L l <_s t /\ E. u e. S u <_s m ) )
328 33 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> L C_ No )
329 simprl 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> t e. L )
330 328 329 sseldd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> t e. No )
331 330 adantrl 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> t e. No )
332 8 adantr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> B e. No )
333 331 332 mulscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( t x.s B ) e. No )
334 6 adantr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> A e. No )
335 181 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> S C_ No )
336 simprr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> u e. S )
337 335 336 sseldd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> u e. No )
338 337 adantrl 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> u e. No )
339 334 338 mulscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( A x.s u ) e. No )
340 333 339 addscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( t x.s B ) +s ( A x.s u ) ) e. No )
341 331 338 mulscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( t x.s u ) e. No )
342 340 341 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No )
343 342 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No )
344 simprl 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> l e. ( _Left ` A ) )
345 16 344 sselid 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> l e. No )
346 8 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> B e. No )
347 345 346 mulscld 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> ( l x.s B ) e. No )
348 347 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( l x.s B ) e. No )
349 348 339 addscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( l x.s B ) +s ( A x.s u ) ) e. No )
350 345 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> l e. No )
351 350 338 mulscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( l x.s u ) e. No )
352 349 351 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) e. No )
353 352 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) e. No )
354 6 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> A e. No )
355 simprr 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> m e. ( _Right ` B ) )
356 160 355 sselid 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> m e. No )
357 354 356 mulscld 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> ( A x.s m ) e. No )
358 357 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( A x.s m ) e. No )
359 348 358 addscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( l x.s B ) +s ( A x.s m ) ) e. No )
360 345 356 mulscld 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> ( l x.s m ) e. No )
361 360 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( l x.s m ) e. No )
362 359 361 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) e. No )
363 362 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) e. No )
364 345 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> l e. No )
365 331 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> t e. No )
366 8 adantr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> B e. No )
367 338 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> u e. No )
368 simprrl 
 |-  ( ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) -> l <_s t )
369 368 adantl 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> l <_s t )
370 8 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B e. No )
371 scutcut 
 |-  ( M < ( ( M |s S ) e. No /\ M <
372 2 371 syl 
 |-  ( ph -> ( ( M |s S ) e. No /\ M <
373 372 simp3d 
 |-  ( ph -> { ( M |s S ) } <
374 373 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> { ( M |s S ) } <
375 ovex 
 |-  ( M |s S ) e. _V
376 375 snid 
 |-  ( M |s S ) e. { ( M |s S ) }
377 4 376 eqeltrdi 
 |-  ( ph -> B e. { ( M |s S ) } )
378 377 adantr 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B e. { ( M |s S ) } )
379 374 378 336 ssltsepcd 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B
380 370 337 379 sltled 
 |-  ( ( ph /\ ( t e. L /\ u e. S ) ) -> B <_s u )
381 380 adantrl 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> B <_s u )
382 381 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> B <_s u )
383 364 365 366 367 369 382 slemuld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( l x.s u ) -s ( l x.s B ) ) <_s ( ( t x.s u ) -s ( t x.s B ) ) )
384 351 348 341 333 slesubsub2bd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s u ) -s ( l x.s B ) ) <_s ( ( t x.s u ) -s ( t x.s B ) ) <-> ( ( t x.s B ) -s ( t x.s u ) ) <_s ( ( l x.s B ) -s ( l x.s u ) ) ) )
385 333 341 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( t x.s B ) -s ( t x.s u ) ) e. No )
386 348 351 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( l x.s B ) -s ( l x.s u ) ) e. No )
387 385 386 339 sleadd1d 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( t x.s B ) -s ( t x.s u ) ) <_s ( ( l x.s B ) -s ( l x.s u ) ) <-> ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) <_s ( ( ( l x.s B ) -s ( l x.s u ) ) +s ( A x.s u ) ) ) )
388 384 387 bitrd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s u ) -s ( l x.s B ) ) <_s ( ( t x.s u ) -s ( t x.s B ) ) <-> ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) <_s ( ( ( l x.s B ) -s ( l x.s u ) ) +s ( A x.s u ) ) ) )
389 388 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s u ) -s ( l x.s B ) ) <_s ( ( t x.s u ) -s ( t x.s B ) ) <-> ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) <_s ( ( ( l x.s B ) -s ( l x.s u ) ) +s ( A x.s u ) ) ) )
390 383 389 mpbid 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) <_s ( ( ( l x.s B ) -s ( l x.s u ) ) +s ( A x.s u ) ) )
391 333 339 341 addsubsd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) = ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) )
392 391 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) = ( ( ( t x.s B ) -s ( t x.s u ) ) +s ( A x.s u ) ) )
393 348 339 351 addsubsd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) = ( ( ( l x.s B ) -s ( l x.s u ) ) +s ( A x.s u ) ) )
394 393 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) = ( ( ( l x.s B ) -s ( l x.s u ) ) +s ( A x.s u ) ) )
395 390 392 394 3brtr4d 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) )
396 6 adantr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> A e. No )
397 356 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> m e. No )
398 ssltleft 
 |-  ( A e. No -> ( _Left ` A ) <
399 6 398 syl 
 |-  ( ph -> ( _Left ` A ) <
400 399 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> ( _Left ` A ) <
401 snidg 
 |-  ( A e. No -> A e. { A } )
402 6 401 syl 
 |-  ( ph -> A e. { A } )
403 402 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> A e. { A } )
404 400 344 403 ssltsepcd 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> l
405 345 354 404 sltled 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> l <_s A )
406 405 adantrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> l <_s A )
407 simprrr 
 |-  ( ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) -> u <_s m )
408 407 adantl 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> u <_s m )
409 364 396 367 397 406 408 slemuld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( l x.s m ) -s ( l x.s u ) ) <_s ( ( A x.s m ) -s ( A x.s u ) ) )
410 361 358 351 339 slesubsub3bd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s m ) -s ( l x.s u ) ) <_s ( ( A x.s m ) -s ( A x.s u ) ) <-> ( ( A x.s u ) -s ( l x.s u ) ) <_s ( ( A x.s m ) -s ( l x.s m ) ) ) )
411 339 351 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( A x.s u ) -s ( l x.s u ) ) e. No )
412 358 361 subscld 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( A x.s m ) -s ( l x.s m ) ) e. No )
413 411 412 348 sleadd2d 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( A x.s u ) -s ( l x.s u ) ) <_s ( ( A x.s m ) -s ( l x.s m ) ) <-> ( ( l x.s B ) +s ( ( A x.s u ) -s ( l x.s u ) ) ) <_s ( ( l x.s B ) +s ( ( A x.s m ) -s ( l x.s m ) ) ) ) )
414 410 413 bitrd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s m ) -s ( l x.s u ) ) <_s ( ( A x.s m ) -s ( A x.s u ) ) <-> ( ( l x.s B ) +s ( ( A x.s u ) -s ( l x.s u ) ) ) <_s ( ( l x.s B ) +s ( ( A x.s m ) -s ( l x.s m ) ) ) ) )
415 414 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s m ) -s ( l x.s u ) ) <_s ( ( A x.s m ) -s ( A x.s u ) ) <-> ( ( l x.s B ) +s ( ( A x.s u ) -s ( l x.s u ) ) ) <_s ( ( l x.s B ) +s ( ( A x.s m ) -s ( l x.s m ) ) ) ) )
416 409 415 mpbid 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( l x.s B ) +s ( ( A x.s u ) -s ( l x.s u ) ) ) <_s ( ( l x.s B ) +s ( ( A x.s m ) -s ( l x.s m ) ) ) )
417 348 339 351 addsubsassd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) = ( ( l x.s B ) +s ( ( A x.s u ) -s ( l x.s u ) ) ) )
418 417 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) = ( ( l x.s B ) +s ( ( A x.s u ) -s ( l x.s u ) ) ) )
419 348 358 361 addsubsassd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( t e. L /\ u e. S ) ) ) -> ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) = ( ( l x.s B ) +s ( ( A x.s m ) -s ( l x.s m ) ) ) )
420 419 adantrrr 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) = ( ( l x.s B ) +s ( ( A x.s m ) -s ( l x.s m ) ) ) )
421 416 418 420 3brtr4d 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( l x.s B ) +s ( A x.s u ) ) -s ( l x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
422 343 353 363 395 421 sletrd 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
423 422 anassrs 
 |-  ( ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) /\ ( ( t e. L /\ u e. S ) /\ ( l <_s t /\ u <_s m ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
424 423 expr 
 |-  ( ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) /\ ( t e. L /\ u e. S ) ) -> ( ( l <_s t /\ u <_s m ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
425 424 reximdvva 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) ) -> ( E. t e. L E. u e. S ( l <_s t /\ u <_s m ) -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
426 425 expcom 
 |-  ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) -> ( ph -> ( E. t e. L E. u e. S ( l <_s t /\ u <_s m ) -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) )
427 426 com23 
 |-  ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) -> ( E. t e. L E. u e. S ( l <_s t /\ u <_s m ) -> ( ph -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) )
428 427 imp 
 |-  ( ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ E. t e. L E. u e. S ( l <_s t /\ u <_s m ) ) -> ( ph -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
429 327 428 sylan2br 
 |-  ( ( ( l e. ( _Left ` A ) /\ m e. ( _Right ` B ) ) /\ ( E. t e. L l <_s t /\ E. u e. S u <_s m ) ) -> ( ph -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
430 429 an4s 
 |-  ( ( ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) /\ ( m e. ( _Right ` B ) /\ E. u e. S u <_s m ) ) -> ( ph -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
431 430 impcom 
 |-  ( ( ph /\ ( ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) /\ ( m e. ( _Right ` B ) /\ E. u e. S u <_s m ) ) ) -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
432 431 anassrs 
 |-  ( ( ( ph /\ ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) ) /\ ( m e. ( _Right ` B ) /\ E. u e. S u <_s m ) ) -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
433 432 expr 
 |-  ( ( ( ph /\ ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) ) /\ m e. ( _Right ` B ) ) -> ( E. u e. S u <_s m -> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
434 433 ralimdva 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) ) -> ( A. m e. ( _Right ` B ) E. u e. S u <_s m -> A. m e. ( _Right ` B ) E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
435 326 434 mpd 
 |-  ( ( ph /\ ( l e. ( _Left ` A ) /\ E. t e. L l <_s t ) ) -> A. m e. ( _Right ` B ) E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
436 435 expr 
 |-  ( ( ph /\ l e. ( _Left ` A ) ) -> ( E. t e. L l <_s t -> A. m e. ( _Right ` B ) E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
437 436 ralimdva 
 |-  ( ph -> ( A. l e. ( _Left ` A ) E. t e. L l <_s t -> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
438 324 437 mpd 
 |-  ( ph -> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
439 eqeq1 
 |-  ( c = z -> ( c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) )
440 439 2rexbidv 
 |-  ( c = z -> ( E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. t e. L E. u e. S z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) )
441 440 rexab 
 |-  ( E. z e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. z ( E. t e. L E. u e. S z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
442 r19.41vv 
 |-  ( E. t e. L E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> ( E. t e. L E. u e. S z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
443 442 exbii 
 |-  ( E. z E. t e. L E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. z ( E. t e. L E. u e. S z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
444 rexcom4 
 |-  ( E. t e. L E. z E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. z E. t e. L E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
445 rexcom4 
 |-  ( E. u e. S E. z ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. z E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
446 ovex 
 |-  ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. _V
447 breq1 
 |-  ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
448 446 447 ceqsexv 
 |-  ( E. z ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
449 448 rexbii 
 |-  ( E. u e. S E. z ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
450 445 449 bitr3i 
 |-  ( E. z E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
451 450 rexbii 
 |-  ( E. t e. L E. z E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
452 444 451 bitr3i 
 |-  ( E. z E. t e. L E. u e. S ( z = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) /\ z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) <-> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
453 441 443 452 3bitr2i 
 |-  ( E. z e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
454 ssun1 
 |-  { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } C_ ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } )
455 ssrexv 
 |-  ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } C_ ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> ( E. z e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
456 454 455 ax-mp 
 |-  ( E. z e. { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
457 453 456 sylbir 
 |-  ( E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
458 457 2ralimi 
 |-  ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. t e. L E. u e. S ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
459 438 458 syl 
 |-  ( ph -> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
460 1 3 cofcutr2d 
 |-  ( ph -> A. x e. ( _Right ` A ) E. v e. R v <_s x )
461 2 4 cofcutr1d 
 |-  ( ph -> A. y e. ( _Left ` B ) E. w e. M y <_s w )
462 461 adantr 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) ) -> A. y e. ( _Left ` B ) E. w e. M y <_s w )
463 reeanv 
 |-  ( E. v e. R E. w e. M ( v <_s x /\ y <_s w ) <-> ( E. v e. R v <_s x /\ E. w e. M y <_s w ) )
464 170 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> R C_ No )
465 simprl 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> v e. R )
466 464 465 sseldd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> v e. No )
467 8 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> B e. No )
468 466 467 mulscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( v x.s B ) e. No )
469 468 adantrl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( v x.s B ) e. No )
470 6 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> A e. No )
471 44 adantr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> M C_ No )
472 simprr 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> w e. M )
473 471 472 sseldd 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> w e. No )
474 470 473 mulscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( A x.s w ) e. No )
475 474 adantrl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( A x.s w ) e. No )
476 469 475 addscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( v x.s B ) +s ( A x.s w ) ) e. No )
477 466 473 mulscld 
 |-  ( ( ph /\ ( v e. R /\ w e. M ) ) -> ( v x.s w ) e. No )
478 477 adantrl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( v x.s w ) e. No )
479 476 478 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No )
480 479 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No )
481 6 adantr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> A e. No )
482 simprr 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> y e. ( _Left ` B ) )
483 23 482 sselid 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> y e. No )
484 483 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> y e. No )
485 481 484 mulscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( A x.s y ) e. No )
486 469 485 addscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( v x.s B ) +s ( A x.s y ) ) e. No )
487 466 adantrl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> v e. No )
488 487 484 mulscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( v x.s y ) e. No )
489 486 488 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) e. No )
490 489 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) e. No )
491 simprl 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> x e. ( _Right ` A ) )
492 153 491 sselid 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> x e. No )
493 8 adantr 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> B e. No )
494 492 493 mulscld 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> ( x x.s B ) e. No )
495 494 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( x x.s B ) e. No )
496 495 485 addscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( x x.s B ) +s ( A x.s y ) ) e. No )
497 492 483 mulscld 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> ( x x.s y ) e. No )
498 497 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( x x.s y ) e. No )
499 496 498 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) e. No )
500 499 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) e. No )
501 6 adantr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> A e. No )
502 487 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> v e. No )
503 483 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> y e. No )
504 473 adantrl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> w e. No )
505 504 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> w e. No )
506 3 sneqd 
 |-  ( ph -> { A } = { ( L |s R ) } )
507 506 222 eqbrtrd 
 |-  ( ph -> { A } <
508 507 adantr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> { A } <
509 481 401 syl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> A e. { A } )
510 simprrl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> v e. R )
511 508 509 510 ssltsepcd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> A
512 481 487 511 sltled 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> A <_s v )
513 512 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> A <_s v )
514 simprrr 
 |-  ( ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) -> y <_s w )
515 514 adantl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> y <_s w )
516 501 502 503 505 513 515 slemuld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( A x.s w ) -s ( A x.s y ) ) <_s ( ( v x.s w ) -s ( v x.s y ) ) )
517 475 478 485 488 slesubsubbd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( A x.s w ) -s ( A x.s y ) ) <_s ( ( v x.s w ) -s ( v x.s y ) ) <-> ( ( A x.s w ) -s ( v x.s w ) ) <_s ( ( A x.s y ) -s ( v x.s y ) ) ) )
518 475 478 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( A x.s w ) -s ( v x.s w ) ) e. No )
519 485 488 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( A x.s y ) -s ( v x.s y ) ) e. No )
520 518 519 469 sleadd2d 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( A x.s w ) -s ( v x.s w ) ) <_s ( ( A x.s y ) -s ( v x.s y ) ) <-> ( ( v x.s B ) +s ( ( A x.s w ) -s ( v x.s w ) ) ) <_s ( ( v x.s B ) +s ( ( A x.s y ) -s ( v x.s y ) ) ) ) )
521 517 520 bitrd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( A x.s w ) -s ( A x.s y ) ) <_s ( ( v x.s w ) -s ( v x.s y ) ) <-> ( ( v x.s B ) +s ( ( A x.s w ) -s ( v x.s w ) ) ) <_s ( ( v x.s B ) +s ( ( A x.s y ) -s ( v x.s y ) ) ) ) )
522 521 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( A x.s w ) -s ( A x.s y ) ) <_s ( ( v x.s w ) -s ( v x.s y ) ) <-> ( ( v x.s B ) +s ( ( A x.s w ) -s ( v x.s w ) ) ) <_s ( ( v x.s B ) +s ( ( A x.s y ) -s ( v x.s y ) ) ) ) )
523 516 522 mpbid 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( v x.s B ) +s ( ( A x.s w ) -s ( v x.s w ) ) ) <_s ( ( v x.s B ) +s ( ( A x.s y ) -s ( v x.s y ) ) ) )
524 469 475 478 addsubsassd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) = ( ( v x.s B ) +s ( ( A x.s w ) -s ( v x.s w ) ) ) )
525 524 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) = ( ( v x.s B ) +s ( ( A x.s w ) -s ( v x.s w ) ) ) )
526 469 485 488 addsubsassd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) = ( ( v x.s B ) +s ( ( A x.s y ) -s ( v x.s y ) ) ) )
527 526 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) = ( ( v x.s B ) +s ( ( A x.s y ) -s ( v x.s y ) ) ) )
528 523 525 527 3brtr4d 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) )
529 492 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> x e. No )
530 8 adantr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> B e. No )
531 simprrl 
 |-  ( ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) -> v <_s x )
532 531 adantl 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> v <_s x )
533 493 61 syl 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> ( _Left ` B ) <
534 65 adantr 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> B e. { B } )
535 533 482 534 ssltsepcd 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> y
536 483 493 535 sltled 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> y <_s B )
537 536 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> y <_s B )
538 502 529 503 530 532 537 slemuld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( v x.s B ) -s ( v x.s y ) ) <_s ( ( x x.s B ) -s ( x x.s y ) ) )
539 469 488 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( v x.s B ) -s ( v x.s y ) ) e. No )
540 539 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( v x.s B ) -s ( v x.s y ) ) e. No )
541 495 498 subscld 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( x x.s B ) -s ( x x.s y ) ) e. No )
542 541 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( x x.s B ) -s ( x x.s y ) ) e. No )
543 485 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( A x.s y ) e. No )
544 540 542 543 sleadd1d 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) -s ( v x.s y ) ) <_s ( ( x x.s B ) -s ( x x.s y ) ) <-> ( ( ( v x.s B ) -s ( v x.s y ) ) +s ( A x.s y ) ) <_s ( ( ( x x.s B ) -s ( x x.s y ) ) +s ( A x.s y ) ) ) )
545 538 544 mpbid 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) -s ( v x.s y ) ) +s ( A x.s y ) ) <_s ( ( ( x x.s B ) -s ( x x.s y ) ) +s ( A x.s y ) ) )
546 469 485 488 addsubsd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( v e. R /\ w e. M ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) = ( ( ( v x.s B ) -s ( v x.s y ) ) +s ( A x.s y ) ) )
547 546 adantrrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) = ( ( ( v x.s B ) -s ( v x.s y ) ) +s ( A x.s y ) ) )
548 6 adantr 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> A e. No )
549 548 483 mulscld 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> ( A x.s y ) e. No )
550 494 549 497 addsubsd 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) = ( ( ( x x.s B ) -s ( x x.s y ) ) +s ( A x.s y ) ) )
551 550 adantrr 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) = ( ( ( x x.s B ) -s ( x x.s y ) ) +s ( A x.s y ) ) )
552 545 547 551 3brtr4d 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s y ) ) -s ( v x.s y ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
553 480 490 500 528 552 sletrd 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
554 553 anassrs 
 |-  ( ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) /\ ( ( v e. R /\ w e. M ) /\ ( v <_s x /\ y <_s w ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
555 554 expr 
 |-  ( ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) /\ ( v e. R /\ w e. M ) ) -> ( ( v <_s x /\ y <_s w ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
556 555 reximdvva 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) ) -> ( E. v e. R E. w e. M ( v <_s x /\ y <_s w ) -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
557 556 expcom 
 |-  ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) -> ( ph -> ( E. v e. R E. w e. M ( v <_s x /\ y <_s w ) -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) )
558 557 com23 
 |-  ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) -> ( E. v e. R E. w e. M ( v <_s x /\ y <_s w ) -> ( ph -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) )
559 558 imp 
 |-  ( ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ E. v e. R E. w e. M ( v <_s x /\ y <_s w ) ) -> ( ph -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
560 463 559 sylan2br 
 |-  ( ( ( x e. ( _Right ` A ) /\ y e. ( _Left ` B ) ) /\ ( E. v e. R v <_s x /\ E. w e. M y <_s w ) ) -> ( ph -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
561 560 an4s 
 |-  ( ( ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) /\ ( y e. ( _Left ` B ) /\ E. w e. M y <_s w ) ) -> ( ph -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
562 561 impcom 
 |-  ( ( ph /\ ( ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) /\ ( y e. ( _Left ` B ) /\ E. w e. M y <_s w ) ) ) -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
563 562 anassrs 
 |-  ( ( ( ph /\ ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) ) /\ ( y e. ( _Left ` B ) /\ E. w e. M y <_s w ) ) -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
564 563 expr 
 |-  ( ( ( ph /\ ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) ) /\ y e. ( _Left ` B ) ) -> ( E. w e. M y <_s w -> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
565 564 ralimdva 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) ) -> ( A. y e. ( _Left ` B ) E. w e. M y <_s w -> A. y e. ( _Left ` B ) E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
566 462 565 mpd 
 |-  ( ( ph /\ ( x e. ( _Right ` A ) /\ E. v e. R v <_s x ) ) -> A. y e. ( _Left ` B ) E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
567 566 expr 
 |-  ( ( ph /\ x e. ( _Right ` A ) ) -> ( E. v e. R v <_s x -> A. y e. ( _Left ` B ) E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
568 567 ralimdva 
 |-  ( ph -> ( A. x e. ( _Right ` A ) E. v e. R v <_s x -> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
569 460 568 mpd 
 |-  ( ph -> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
570 eqeq1 
 |-  ( d = z -> ( d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
571 570 2rexbidv 
 |-  ( d = z -> ( E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. v e. R E. w e. M z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
572 571 rexab 
 |-  ( E. z e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. z ( E. v e. R E. w e. M z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
573 r19.41vv 
 |-  ( E. v e. R E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> ( E. v e. R E. w e. M z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
574 573 exbii 
 |-  ( E. z E. v e. R E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. z ( E. v e. R E. w e. M z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
575 rexcom4 
 |-  ( E. v e. R E. z E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. z E. v e. R E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
576 rexcom4 
 |-  ( E. w e. M E. z ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. z E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
577 ovex 
 |-  ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. _V
578 breq1 
 |-  ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
579 577 578 ceqsexv 
 |-  ( E. z ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
580 579 rexbii 
 |-  ( E. w e. M E. z ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
581 576 580 bitr3i 
 |-  ( E. z E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
582 581 rexbii 
 |-  ( E. v e. R E. z E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
583 575 582 bitr3i 
 |-  ( E. z E. v e. R E. w e. M ( z = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) /\ z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) <-> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
584 572 574 583 3bitr2i 
 |-  ( E. z e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
585 ssun2 
 |-  { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } C_ ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } )
586 ssrexv 
 |-  ( { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } C_ ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) -> ( E. z e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
587 585 586 ax-mp 
 |-  ( E. z e. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
588 584 587 sylbir 
 |-  ( E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
589 588 2ralimi 
 |-  ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. v e. R E. w e. M ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
590 569 589 syl 
 |-  ( ph -> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
591 ralunb 
 |-  ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
592 eqeq1 
 |-  ( k = xO -> ( k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
593 592 2rexbidv 
 |-  ( k = xO -> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
594 593 ralab 
 |-  ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
595 r19.23v 
 |-  ( A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
596 595 ralbii 
 |-  ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
597 r19.23v 
 |-  ( A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
598 596 597 bitri 
 |-  ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
599 598 albii 
 |-  ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
600 ralcom4 
 |-  ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
601 ralcom4 
 |-  ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
602 ovex 
 |-  ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) e. _V
603 breq2 
 |-  ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( z <_s xO <-> z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
604 603 rexbidv 
 |-  ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) )
605 602 604 ceqsalv 
 |-  ( A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
606 605 ralbii 
 |-  ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
607 601 606 bitr3i 
 |-  ( A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
608 607 ralbii 
 |-  ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
609 600 608 bitr3i 
 |-  ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
610 594 599 609 3bitr2i 
 |-  ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) )
611 eqeq1 
 |-  ( n = xO -> ( n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
612 611 2rexbidv 
 |-  ( n = xO -> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
613 612 ralab 
 |-  ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
614 r19.23v 
 |-  ( A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
615 614 ralbii 
 |-  ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
616 r19.23v 
 |-  ( A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
617 615 616 bitri 
 |-  ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
618 617 albii 
 |-  ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
619 ralcom4 
 |-  ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
620 ralcom4 
 |-  ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) )
621 ovex 
 |-  ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) e. _V
622 breq2 
 |-  ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( z <_s xO <-> z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
623 622 rexbidv 
 |-  ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
624 621 623 ceqsalv 
 |-  ( A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
625 624 ralbii 
 |-  ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
626 620 625 bitr3i 
 |-  ( A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
627 626 ralbii 
 |-  ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
628 619 627 bitr3i 
 |-  ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
629 613 618 628 3bitr2i 
 |-  ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) )
630 610 629 anbi12i 
 |-  ( ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
631 591 630 bitri 
 |-  ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) )
632 459 590 631 sylanbrc 
 |-  ( ph -> A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO )
633 1 2 3 4 ssltmul1 
 |-  ( ph -> ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
634 10 sneqd 
 |-  ( ph -> { ( A x.s B ) } = { ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) |s ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) ) } )
635 633 634 breqtrd 
 |-  ( ph -> ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
636 1 2 3 4 ssltmul2 
 |-  ( ph -> { ( A x.s B ) } <
637 634 636 eqbrtrrd 
 |-  ( ph -> { ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) |s ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) ) } <
638 11 323 632 635 637 cofcut1d 
 |-  ( ph -> ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) |s ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) ) = ( ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) )
639 10 638 eqtrd 
 |-  ( ph -> ( A x.s B ) = ( ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) )