Metamath Proof Explorer

Theorem mulsproplem9

Description: Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 
|- ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
mulsproplem9.1 
|- ( ph -> A e. No )
mulsproplem9.2 
|- ( ph -> B e. No )
Assertion mulsproplem9 
|- ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

Step Hyp Ref Expression
1 mulsproplem.1 
 |-  ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
2 mulsproplem9.1 
 |-  ( ph -> A e. No )
3 mulsproplem9.2 
 |-  ( ph -> B e. No )
4 eqid 
 |-  ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) = ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
5 4 rnmpo 
 |-  ran ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) = { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) }
6 fvex 
 |-  ( _Left ` A ) e. _V
7 fvex 
 |-  ( _Left ` B ) e. _V
8 6 7 mpoex 
 |-  ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) e. _V
9 8 rnex 
 |-  ran ( p e. ( _Left ` A ) , q e. ( _Left ` B ) |-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) e. _V
10 5 9 eqeltrri 
 |-  { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } e. _V
11 eqid 
 |-  ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) = ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
12 11 rnmpo 
 |-  ran ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) = { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) }
13 fvex 
 |-  ( _Right ` A ) e. _V
14 fvex 
 |-  ( _Right ` B ) e. _V
15 13 14 mpoex 
 |-  ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) e. _V
16 15 rnex 
 |-  ran ( r e. ( _Right ` A ) , s e. ( _Right ` B ) |-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) e. _V
17 12 16 eqeltrri 
 |-  { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } e. _V
18 10 17 unex 
 |-  ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) e. _V
19 18 a1i 
 |-  ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) e. _V )
20 eqid 
 |-  ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) )
21 20 rnmpo 
 |-  ran ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) = { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) }
22 6 14 mpoex 
 |-  ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V
23 22 rnex 
 |-  ran ( t e. ( _Left ` A ) , u e. ( _Right ` B ) |-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) e. _V
24 21 23 eqeltrri 
 |-  { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } e. _V
25 eqid 
 |-  ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) )
26 25 rnmpo 
 |-  ran ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) = { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) }
27 13 7 mpoex 
 |-  ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V
28 27 rnex 
 |-  ran ( v e. ( _Right ` A ) , w e. ( _Left ` B ) |-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) e. _V
29 26 28 eqeltrri 
 |-  { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } e. _V
30 24 29 unex 
 |-  ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V
31 30 a1i 
 |-  ( ph -> ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) e. _V )
32 1 adantr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
33 simprl 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Left ` A ) )
34 33 leftoldd 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Old ` ( bday ` A ) ) )
35 3 adantr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> B e. No )
36 32 34 35 mulsproplem2 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s B ) e. No )
37 2 adantr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> A e. No )
38 simprr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Left ` B ) )
39 38 leftoldd 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Old ` ( bday ` B ) ) )
40 32 37 39 mulsproplem3 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( A x.s q ) e. No )
41 36 40 addscld 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( p x.s B ) +s ( A x.s q ) ) e. No )
42 32 34 39 mulsproplem4 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s q ) e. No )
43 41 42 subscld 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No )
44 eleq1 
 |-  ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( g e. No <-> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) e. No ) )
45 43 44 syl5ibrcom 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> g e. No ) )
46 45 rexlimdvva 
 |-  ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> g e. No ) )
47 46 abssdv 
 |-  ( ph -> { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } C_ No )
48 1 adantr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
49 simprl 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Right ` A ) )
50 49 rightoldd 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Old ` ( bday ` A ) ) )
51 3 adantr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> B e. No )
52 48 50 51 mulsproplem2 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s B ) e. No )
53 2 adantr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> A e. No )
54 simprr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Right ` B ) )
55 54 rightoldd 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Old ` ( bday ` B ) ) )
56 48 53 55 mulsproplem3 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( A x.s s ) e. No )
57 52 56 addscld 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( r x.s B ) +s ( A x.s s ) ) e. No )
58 48 50 55 mulsproplem4 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s s ) e. No )
59 57 58 subscld 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No )
60 eleq1 
 |-  ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( h e. No <-> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) e. No ) )
61 59 60 syl5ibrcom 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> h e. No ) )
62 61 rexlimdvva 
 |-  ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> h e. No ) )
63 62 abssdv 
 |-  ( ph -> { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } C_ No )
64 47 63 unssd 
 |-  ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) C_ No )
65 1 adantr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
66 simprl 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Left ` A ) )
67 66 leftoldd 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Old ` ( bday ` A ) ) )
68 3 adantr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> B e. No )
69 65 67 68 mulsproplem2 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s B ) e. No )
70 2 adantr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> A e. No )
71 simprr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Right ` B ) )
72 71 rightoldd 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Old ` ( bday ` B ) ) )
73 65 70 72 mulsproplem3 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( A x.s u ) e. No )
74 69 73 addscld 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( t x.s B ) +s ( A x.s u ) ) e. No )
75 65 67 72 mulsproplem4 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s u ) e. No )
76 74 75 subscld 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No )
77 eleq1 
 |-  ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( i e. No <-> ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) e. No ) )
78 76 77 syl5ibrcom 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> i e. No ) )
79 78 rexlimdvva 
 |-  ( ph -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> i e. No ) )
80 79 abssdv 
 |-  ( ph -> { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } C_ No )
81 1 adantr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
82 simprl 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Right ` A ) )
83 82 rightoldd 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Old ` ( bday ` A ) ) )
84 3 adantr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> B e. No )
85 81 83 84 mulsproplem2 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s B ) e. No )
86 2 adantr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> A e. No )
87 simprr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Left ` B ) )
88 87 leftoldd 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Old ` ( bday ` B ) ) )
89 81 86 88 mulsproplem3 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( A x.s w ) e. No )
90 85 89 addscld 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( v x.s B ) +s ( A x.s w ) ) e. No )
91 81 83 88 mulsproplem4 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s w ) e. No )
92 90 91 subscld 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No )
93 eleq1 
 |-  ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( j e. No <-> ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) e. No ) )
94 92 93 syl5ibrcom 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> j e. No ) )
95 94 rexlimdvva 
 |-  ( ph -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> j e. No ) )
96 95 abssdv 
 |-  ( ph -> { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } C_ No )
97 80 96 unssd 
 |-  ( ph -> ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) C_ No )
98 elun 
 |-  ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } \/ x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) )
99 vex 
 |-  x e. _V
100 eqeq1 
 |-  ( g = x -> ( g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
101 100 2rexbidv 
 |-  ( g = x -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
102 99 101 elab 
 |-  ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } <-> E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) )
103 eqeq1 
 |-  ( h = x -> ( h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
104 103 2rexbidv 
 |-  ( h = x -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
105 99 104 elab 
 |-  ( x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } <-> E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
106 102 105 orbi12i 
 |-  ( ( x e. { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } \/ x e. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
107 98 106 bitri 
 |-  ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <-> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
108 elun 
 |-  ( y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) )
109 vex 
 |-  y e. _V
110 eqeq1 
 |-  ( i = y -> ( i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) )
111 110 2rexbidv 
 |-  ( i = y -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) )
112 109 111 elab 
 |-  ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) )
113 eqeq1 
 |-  ( j = y -> ( j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
114 113 2rexbidv 
 |-  ( j = y -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
115 109 114 elab 
 |-  ( y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) )
116 112 115 orbi12i 
 |-  ( ( y e. { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } \/ y e. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
117 108 116 bitri 
 |-  ( y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) <-> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) )
118 107 117 anbi12i 
 |-  ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) <-> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) /\ ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) )
119 anddi 
 |-  ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) \/ E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) /\ ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) \/ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) <-> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) )
120 118 119 bitri 
 |-  ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) <-> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) )
121 1 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
122 2 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No )
123 3 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No )
124 simprll 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> p e. ( _Left ` A ) )
125 simprlr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> q e. ( _Left ` B ) )
126 simprrl 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) )
127 simprrr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) )
128 121 122 123 124 125 126 127 mulsproplem5 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
129 breq2 
 |-  ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( ( 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 ) )
130 128 129 syl5ibrcom 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
131 130 anassrs 
 |-  ( ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
132 131 rexlimdvva 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
133 breq1 
 |-  ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( x  ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
134 133 imbi2d 
 |-  ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x  ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
135 132 134 syl5ibrcom 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
136 135 rexlimdvva 
 |-  ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
137 136 impd 
 |-  ( ph -> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) -> x
138 1 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
139 2 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No )
140 3 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No )
141 simprll 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> p e. ( _Left ` A ) )
142 simprlr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> q e. ( _Left ` B ) )
143 simprrl 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) )
144 simprrr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) )
145 138 139 140 141 142 143 144 mulsproplem6 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
146 breq2 
 |-  ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( ( 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 ) )
147 145 146 syl5ibrcom 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
148 147 anassrs 
 |-  ( ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
149 148 rexlimdvva 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
150 133 imbi2d 
 |-  ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x  ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) )
151 149 150 syl5ibrcom 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
152 151 rexlimdvva 
 |-  ( ph -> ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
153 152 impd 
 |-  ( ph -> ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> x
154 137 153 jaod 
 |-  ( ph -> ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) -> x
155 1 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
156 2 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No )
157 3 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No )
158 simprll 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> r e. ( _Right ` A ) )
159 simprlr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> s e. ( _Right ` B ) )
160 simprrl 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) )
161 simprrr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) )
162 155 156 157 158 159 160 161 mulsproplem7 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
163 breq2 
 |-  ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( ( 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 ) )
164 162 163 syl5ibrcom 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
165 164 anassrs 
 |-  ( ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
166 165 rexlimdvva 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
167 breq1 
 |-  ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( x  ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
168 167 imbi2d 
 |-  ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x  ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
169 166 168 syl5ibrcom 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
170 169 rexlimdvva 
 |-  ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) -> x
171 170 impd 
 |-  ( ph -> ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) -> x
172 1 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
173 2 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No )
174 3 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No )
175 simprll 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> r e. ( _Right ` A ) )
176 simprlr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> s e. ( _Right ` B ) )
177 simprrl 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) )
178 simprrr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) )
179 172 173 174 175 176 177 178 mulsproplem8 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
180 breq2 
 |-  ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( ( 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 ) )
181 179 180 syl5ibrcom 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
182 181 anassrs 
 |-  ( ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
183 182 rexlimdvva 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
184 167 imbi2d 
 |-  ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x  ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) )
185 183 184 syl5ibrcom 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
186 185 rexlimdvva 
 |-  ( ph -> ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) -> ( E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) -> x
187 186 impd 
 |-  ( ph -> ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) -> x
188 171 187 jaod 
 |-  ( ph -> ( ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) -> x
189 154 188 jaod 
 |-  ( ph -> ( ( ( ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) x = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) \/ ( ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) y = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) \/ ( E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) x = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) /\ E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) y = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) ) ) -> x
190 120 189 biimtrid 
 |-  ( ph -> ( ( x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) -> x
191 190 3impib 
 |-  ( ( ph /\ x e. ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) /\ y e. ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) -> x
192 19 31 64 97 191 sltsd 
 |-  ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <