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