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 leftssold 
 |-  ( _Left ` A ) C_ ( _Old ` ( bday ` A ) )
34 simprl 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Left ` A ) )
35 33 34 sselid 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> p e. ( _Old ` ( bday ` A ) ) )
36 3 adantr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> B e. No )
37 32 35 36 mulsproplem2 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s B ) e. No )
38 2 adantr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> A e. No )
39 leftssold 
 |-  ( _Left ` B ) C_ ( _Old ` ( bday ` B ) )
40 simprr 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Left ` B ) )
41 39 40 sselid 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> q e. ( _Old ` ( bday ` B ) ) )
42 32 38 41 mulsproplem3 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( A x.s q ) e. No )
43 37 42 addscld 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( ( p x.s B ) +s ( A x.s q ) ) e. No )
44 32 35 41 mulsproplem4 
 |-  ( ( ph /\ ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) ) -> ( p x.s q ) e. No )
45 43 44 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 )
46 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 ) )
47 45 46 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 ) )
48 47 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 ) )
49 48 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 )
50 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 ) )
51 rightssold 
 |-  ( _Right ` A ) C_ ( _Old ` ( bday ` A ) )
52 simprl 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Right ` A ) )
53 51 52 sselid 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> r e. ( _Old ` ( bday ` A ) ) )
54 3 adantr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> B e. No )
55 50 53 54 mulsproplem2 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s B ) e. No )
56 2 adantr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> A e. No )
57 rightssold 
 |-  ( _Right ` B ) C_ ( _Old ` ( bday ` B ) )
58 simprr 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Right ` B ) )
59 57 58 sselid 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> s e. ( _Old ` ( bday ` B ) ) )
60 50 56 59 mulsproplem3 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( A x.s s ) e. No )
61 55 60 addscld 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( ( r x.s B ) +s ( A x.s s ) ) e. No )
62 50 53 59 mulsproplem4 
 |-  ( ( ph /\ ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) ) -> ( r x.s s ) e. No )
63 61 62 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 )
64 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 ) )
65 63 64 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 ) )
66 65 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 ) )
67 66 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 )
68 49 67 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 )
69 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 ) )
70 simprl 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Left ` A ) )
71 33 70 sselid 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> t e. ( _Old ` ( bday ` A ) ) )
72 3 adantr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> B e. No )
73 69 71 72 mulsproplem2 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s B ) e. No )
74 2 adantr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> A e. No )
75 simprr 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Right ` B ) )
76 57 75 sselid 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> u e. ( _Old ` ( bday ` B ) ) )
77 69 74 76 mulsproplem3 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( A x.s u ) e. No )
78 73 77 addscld 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( ( t x.s B ) +s ( A x.s u ) ) e. No )
79 69 71 76 mulsproplem4 
 |-  ( ( ph /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) -> ( t x.s u ) e. No )
80 78 79 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 )
81 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 ) )
82 80 81 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 ) )
83 82 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 ) )
84 83 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 )
85 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 ) )
86 simprl 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Right ` A ) )
87 51 86 sselid 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> v e. ( _Old ` ( bday ` A ) ) )
88 3 adantr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> B e. No )
89 85 87 88 mulsproplem2 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s B ) e. No )
90 2 adantr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> A e. No )
91 simprr 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Left ` B ) )
92 39 91 sselid 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> w e. ( _Old ` ( bday ` B ) ) )
93 85 90 92 mulsproplem3 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( A x.s w ) e. No )
94 89 93 addscld 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( ( v x.s B ) +s ( A x.s w ) ) e. No )
95 85 87 92 mulsproplem4 
 |-  ( ( ph /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) -> ( v x.s w ) e. No )
96 94 95 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 )
97 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 ) )
98 96 97 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 ) )
99 98 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 ) )
100 99 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 )
101 84 100 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 )
102 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 ) ) } ) )
103 vex 
 |-  x e. _V
104 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 ) ) ) )
105 104 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 ) ) ) )
106 103 105 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 ) ) )
107 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 ) ) ) )
108 107 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 ) ) ) )
109 103 108 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 ) ) )
110 106 109 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 ) ) ) )
111 102 110 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 ) ) ) )
112 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 ) ) } ) )
113 vex 
 |-  y e. _V
114 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 ) ) ) )
115 114 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 ) ) ) )
116 113 115 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 ) ) )
117 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 ) ) ) )
118 117 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 ) ) ) )
119 113 118 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 ) ) )
120 116 119 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 ) ) ) )
121 112 120 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 ) ) ) )
122 111 121 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 ) ) ) ) )
123 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 ) ) ) ) ) )
124 122 123 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 ) ) ) ) ) )
125 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 ) )
126 2 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No )
127 3 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No )
128 simprll 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> p e. ( _Left ` A ) )
129 simprlr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> q e. ( _Left ` B ) )
130 simprrl 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) )
131 simprrr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) )
132 125 126 127 128 129 130 131 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 ) )
133 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 ) )
134 132 133 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 ) )
135 134 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 ) )
136 135 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 ) )
137 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 ) )
138 137 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 ) )
139 136 138 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
140 139 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
141 140 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
142 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 ) )
143 2 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No )
144 3 adantr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No )
145 simprll 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> p e. ( _Left ` A ) )
146 simprlr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> q e. ( _Left ` B ) )
147 simprrl 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) )
148 simprrr 
 |-  ( ( ph /\ ( ( p e. ( _Left ` A ) /\ q e. ( _Left ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) )
149 142 143 144 145 146 147 148 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 ) )
150 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 ) )
151 149 150 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 ) )
152 151 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 ) )
153 152 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 ) )
154 137 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 ) )
155 153 154 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
156 155 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
157 156 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
158 141 157 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
159 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 ) )
160 2 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> A e. No )
161 3 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> B e. No )
162 simprll 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> r e. ( _Right ` A ) )
163 simprlr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> s e. ( _Right ` B ) )
164 simprrl 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> t e. ( _Left ` A ) )
165 simprrr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( t e. ( _Left ` A ) /\ u e. ( _Right ` B ) ) ) ) -> u e. ( _Right ` B ) )
166 159 160 161 162 163 164 165 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 ) )
167 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 ) )
168 166 167 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 ) )
169 168 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 ) )
170 169 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 ) )
171 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 ) )
172 171 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 ) )
173 170 172 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
174 173 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
175 174 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
176 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 ) )
177 2 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> A e. No )
178 3 adantr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> B e. No )
179 simprll 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> r e. ( _Right ` A ) )
180 simprlr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> s e. ( _Right ` B ) )
181 simprrl 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> v e. ( _Right ` A ) )
182 simprrr 
 |-  ( ( ph /\ ( ( r e. ( _Right ` A ) /\ s e. ( _Right ` B ) ) /\ ( v e. ( _Right ` A ) /\ w e. ( _Left ` B ) ) ) ) -> w e. ( _Left ` B ) )
183 176 177 178 179 180 181 182 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 ) )
184 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 ) )
185 183 184 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 ) )
186 185 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 ) )
187 186 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 ) )
188 171 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 ) )
189 187 188 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
190 189 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
191 190 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
192 175 191 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
193 158 192 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
194 124 193 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
195 194 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
196 19 31 68 101 195 ssltd 
 |-  ( 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 ) ) } ) <