Metamath Proof Explorer

Theorem mulsproplem12

Description: Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming C and D are not the same age and E and F are not the same age. (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 ) )
mulsproplem.2 
|- ( ph -> C e. No )
mulsproplem.3 
|- ( ph -> D e. No )
mulsproplem.4 
|- ( ph -> E e. No )
mulsproplem.5 
|- ( ph -> F e. No )
mulsproplem.6 
|- ( ph -> C
mulsproplem.7 
|- ( ph -> E
mulsproplem12.1 
|- ( ph -> ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) )
mulsproplem12.2 
|- ( ph -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
Assertion mulsproplem12 
|- ( ph -> ( ( C x.s F ) -s ( C x.s E ) )

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 mulsproplem.2 
 |-  ( ph -> C e. No )
3 mulsproplem.3 
 |-  ( ph -> D e. No )
4 mulsproplem.4 
 |-  ( ph -> E e. No )
5 mulsproplem.5 
 |-  ( ph -> F e. No )
6 mulsproplem.6 
 |-  ( ph -> C
7 mulsproplem.7 
 |-  ( ph -> E
8 mulsproplem12.1 
 |-  ( ph -> ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) )
9 mulsproplem12.2 
 |-  ( ph -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
10 unidm 
 |-  ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) )
11 unidm 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) )
12 bday0s 
 |-  ( bday ` 0s ) = (/)
13 12 12 oveq12i 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) )
14 0elon 
 |-  (/) e. On
15 naddrid 
 |-  ( (/) e. On -> ( (/) +no (/) ) = (/) )
16 14 15 ax-mp 
 |-  ( (/) +no (/) ) = (/)
17 13 16 eqtri 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/)
18 11 17 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/)
19 10 18 eqtri 
 |-  ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/)
20 19 uneq2i 
 |-  ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) )
21 un0 
 |-  ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) )
22 20 21 eqtri 
 |-  ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` F ) )
23 ssun2 
 |-  ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
24 ssun1 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
25 23 24 sstri 
 |-  ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
26 ssun2 
 |-  ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( 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 ) ) ) ) )
27 25 26 sstri 
 |-  ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( 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 ) ) ) ) )
28 22 27 eqsstri 
 |-  ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) )
29 28 sseli 
 |-  ( ( ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) )
30 29 imim1i 
 |-  ( ( ( ( ( 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 ) )  ( ( ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
31 30 6ralimi 
 |-  ( 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 ) )  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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
32 1 31 syl 
 |-  ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
33 32 3 5 mulsproplem10 
 |-  ( ph -> ( ( D x.s F ) e. No /\ ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
34 33 simp2d 
 |-  ( ph -> ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
35 34 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
36 simprl 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` C ) e. ( bday ` D ) )
37 bdayelon 
 |-  ( bday ` D ) e. On
38 2 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C e. No )
39 oldbday 
 |-  ( ( ( bday ` D ) e. On /\ C e. No ) -> ( C e. ( _Old ` ( bday ` D ) ) <-> ( bday ` C ) e. ( bday ` D ) ) )
40 37 38 39 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C e. ( _Old ` ( bday ` D ) ) <-> ( bday ` C ) e. ( bday ` D ) ) )
41 36 40 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C e. ( _Old ` ( bday ` D ) ) )
42 6 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C
43 breq1 
 |-  ( x = C -> ( x  C
44 leftval 
 |-  ( _Left ` D ) = { x e. ( _Old ` ( bday ` D ) ) | x
45 43 44 elrab2 
 |-  ( C e. ( _Left ` D ) <-> ( C e. ( _Old ` ( bday ` D ) ) /\ C
46 41 42 45 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C e. ( _Left ` D ) )
47 simprr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` E ) e. ( bday ` F ) )
48 bdayelon 
 |-  ( bday ` F ) e. On
49 4 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. No )
50 oldbday 
 |-  ( ( ( bday ` F ) e. On /\ E e. No ) -> ( E e. ( _Old ` ( bday ` F ) ) <-> ( bday ` E ) e. ( bday ` F ) ) )
51 48 49 50 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( E e. ( _Old ` ( bday ` F ) ) <-> ( bday ` E ) e. ( bday ` F ) ) )
52 47 51 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Old ` ( bday ` F ) ) )
53 7 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E
54 breq1 
 |-  ( x = E -> ( x  E
55 leftval 
 |-  ( _Left ` F ) = { x e. ( _Old ` ( bday ` F ) ) | x
56 54 55 elrab2 
 |-  ( E e. ( _Left ` F ) <-> ( E e. ( _Old ` ( bday ` F ) ) /\ E
57 52 53 56 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) )
58 eqid 
 |-  ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) )
59 oveq1 
 |-  ( p = C -> ( p x.s F ) = ( C x.s F ) )
60 59 oveq1d 
 |-  ( p = C -> ( ( p x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s q ) ) )
61 oveq1 
 |-  ( p = C -> ( p x.s q ) = ( C x.s q ) )
62 60 61 oveq12d 
 |-  ( p = C -> ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) )
63 62 eqeq2d 
 |-  ( p = C -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) ) )
64 oveq2 
 |-  ( q = E -> ( D x.s q ) = ( D x.s E ) )
65 64 oveq2d 
 |-  ( q = E -> ( ( C x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s E ) ) )
66 oveq2 
 |-  ( q = E -> ( C x.s q ) = ( C x.s E ) )
67 65 66 oveq12d 
 |-  ( q = E -> ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) )
68 67 eqeq2d 
 |-  ( q = E -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s q ) ) -s ( C x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) )
69 63 68 rspc2ev 
 |-  ( ( C e. ( _Left ` D ) /\ E e. ( _Left ` F ) /\ ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) )
70 58 69 mp3an3 
 |-  ( ( C e. ( _Left ` D ) /\ E e. ( _Left ` F ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) )
71 46 57 70 syl2anc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) )
72 ovex 
 |-  ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. _V
73 eqeq1 
 |-  ( g = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) -> ( g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) )
74 73 2rexbidv 
 |-  ( g = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) -> ( E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) ) )
75 72 74 elab 
 |-  ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } <-> E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) )
76 71 75 sylibr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } )
77 elun1 
 |-  ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) )
78 76 77 syl 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) )
79 ovex 
 |-  ( D x.s F ) e. _V
80 79 snid 
 |-  ( D x.s F ) e. { ( D x.s F ) }
81 80 a1i 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( D x.s F ) e. { ( D x.s F ) } )
82 35 78 81 ssltsepcd 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) )
83 19 uneq2i 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) )
84 un0 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) )
85 83 84 eqtri 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` F ) )
86 ssun1 
 |-  ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
87 ssun2 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
88 86 87 sstri 
 |-  ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
89 88 26 sstri 
 |-  ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( 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 ) ) ) ) )
90 85 89 eqsstri 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) )
91 90 sseli 
 |-  ( ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) )
92 91 imim1i 
 |-  ( ( ( ( ( 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 ) )  ( ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
93 92 6ralimi 
 |-  ( 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 ) )  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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
94 1 93 syl 
 |-  ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
95 94 2 5 mulsproplem10 
 |-  ( ph -> ( ( C x.s F ) e. No /\ ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` F ) g = ( ( ( p x.s F ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` F ) h = ( ( ( r x.s F ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
96 95 simp1d 
 |-  ( ph -> ( C x.s F ) e. No )
97 19 uneq2i 
 |-  ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) )
98 un0 
 |-  ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) )
99 97 98 eqtri 
 |-  ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` E ) )
100 ssun2 
 |-  ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
101 100 87 sstri 
 |-  ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
102 101 26 sstri 
 |-  ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( 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 ) ) ) ) )
103 99 102 eqsstri 
 |-  ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) )
104 103 sseli 
 |-  ( ( ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) )
105 104 imim1i 
 |-  ( ( ( ( ( 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 ) )  ( ( ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
106 105 6ralimi 
 |-  ( 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 ) )  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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
107 1 106 syl 
 |-  ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
108 107 3 4 mulsproplem10 
 |-  ( ph -> ( ( D x.s E ) e. No /\ ( { g | E. p e. ( _Left ` D ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( D x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` D ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( D x.s s ) ) -s ( r x.s s ) ) } ) <
109 108 simp1d 
 |-  ( ph -> ( D x.s E ) e. No )
110 96 109 addscomd 
 |-  ( ph -> ( ( C x.s F ) +s ( D x.s E ) ) = ( ( D x.s E ) +s ( C x.s F ) ) )
111 110 oveq1d 
 |-  ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( C x.s E ) ) )
112 19 uneq2i 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) )
113 un0 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) )
114 112 113 eqtri 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` E ) )
115 ssun1 
 |-  ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
116 115 24 sstri 
 |-  ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
117 116 26 sstri 
 |-  ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( 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 ) ) ) ) )
118 114 117 eqsstri 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ) ) ) ) )
119 118 sseli 
 |-  ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) )
120 119 imim1i 
 |-  ( ( ( ( ( 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 ) )  ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
121 120 6ralimi 
 |-  ( 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 ) )  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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
122 1 121 syl 
 |-  ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
123 122 2 4 mulsproplem10 
 |-  ( ph -> ( ( C x.s E ) e. No /\ ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
124 123 simp1d 
 |-  ( ph -> ( C x.s E ) e. No )
125 109 96 124 addsubsassd 
 |-  ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( C x.s E ) ) = ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) )
126 111 125 eqtrd 
 |-  ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) = ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) ) )
127 126 breq1d 
 |-  ( ph -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) )  ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) )
128 96 124 subscld 
 |-  ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No )
129 33 simp1d 
 |-  ( ph -> ( D x.s F ) e. No )
130 109 128 129 sltaddsub2d 
 |-  ( ph -> ( ( ( D x.s E ) +s ( ( C x.s F ) -s ( C x.s E ) ) )  ( ( C x.s F ) -s ( C x.s E ) )
131 127 130 bitrd 
 |-  ( ph -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) )  ( ( C x.s F ) -s ( C x.s E ) )
132 131 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) )  ( ( C x.s F ) -s ( C x.s E ) )
133 82 132 mpbid 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
134 133 anassrs 
 |-  ( ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) /\ ( bday ` E ) e. ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
135 108 simp3d 
 |-  ( ph -> { ( D x.s E ) } <
136 135 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> { ( D x.s E ) } <
137 ovex 
 |-  ( D x.s E ) e. _V
138 137 snid 
 |-  ( D x.s E ) e. { ( D x.s E ) }
139 138 a1i 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E ) e. { ( D x.s E ) } )
140 simprl 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` C ) e. ( bday ` D ) )
141 2 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. No )
142 37 141 39 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( C e. ( _Old ` ( bday ` D ) ) <-> ( bday ` C ) e. ( bday ` D ) ) )
143 140 142 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. ( _Old ` ( bday ` D ) ) )
144 6 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C
145 143 144 45 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. ( _Left ` D ) )
146 simprr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` F ) e. ( bday ` E ) )
147 bdayelon 
 |-  ( bday ` E ) e. On
148 5 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. No )
149 oldbday 
 |-  ( ( ( bday ` E ) e. On /\ F e. No ) -> ( F e. ( _Old ` ( bday ` E ) ) <-> ( bday ` F ) e. ( bday ` E ) ) )
150 147 148 149 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( F e. ( _Old ` ( bday ` E ) ) <-> ( bday ` F ) e. ( bday ` E ) ) )
151 146 150 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Old ` ( bday ` E ) ) )
152 7 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E
153 breq2 
 |-  ( x = F -> ( E  E
154 rightval 
 |-  ( _Right ` E ) = { x e. ( _Old ` ( bday ` E ) ) | E
155 153 154 elrab2 
 |-  ( F e. ( _Right ` E ) <-> ( F e. ( _Old ` ( bday ` E ) ) /\ E
156 151 152 155 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) )
157 eqid 
 |-  ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) )
158 oveq1 
 |-  ( t = C -> ( t x.s E ) = ( C x.s E ) )
159 158 oveq1d 
 |-  ( t = C -> ( ( t x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s u ) ) )
160 oveq1 
 |-  ( t = C -> ( t x.s u ) = ( C x.s u ) )
161 159 160 oveq12d 
 |-  ( t = C -> ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) )
162 161 eqeq2d 
 |-  ( t = C -> ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) ) )
163 oveq2 
 |-  ( u = F -> ( D x.s u ) = ( D x.s F ) )
164 163 oveq2d 
 |-  ( u = F -> ( ( C x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s F ) ) )
165 oveq2 
 |-  ( u = F -> ( C x.s u ) = ( C x.s F ) )
166 164 165 oveq12d 
 |-  ( u = F -> ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) )
167 166 eqeq2d 
 |-  ( u = F -> ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s u ) ) -s ( C x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) )
168 162 167 rspc2ev 
 |-  ( ( C e. ( _Left ` D ) /\ F e. ( _Right ` E ) /\ ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) )
169 157 168 mp3an3 
 |-  ( ( C e. ( _Left ` D ) /\ F e. ( _Right ` E ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) )
170 145 156 169 syl2anc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) )
171 ovex 
 |-  ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. _V
172 eqeq1 
 |-  ( i = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) -> ( i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) )
173 172 2rexbidv 
 |-  ( i = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) -> ( E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) <-> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) ) )
174 171 173 elab 
 |-  ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } <-> E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) )
175 170 174 sylibr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } )
176 elun1 
 |-  ( ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. ( { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` D ) E. w e. ( _Left ` E ) j = ( ( ( v x.s E ) +s ( D x.s w ) ) -s ( v x.s w ) ) } ) )
177 175 176 syl 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. ( { i | E. t e. ( _Left ` D ) E. u e. ( _Right ` E ) i = ( ( ( t x.s E ) +s ( D x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` D ) E. w e. ( _Left ` E ) j = ( ( ( v x.s E ) +s ( D x.s w ) ) -s ( v x.s w ) ) } ) )
178 136 139 177 ssltsepcd 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E )
179 124 129 addscomd 
 |-  ( ph -> ( ( C x.s E ) +s ( D x.s F ) ) = ( ( D x.s F ) +s ( C x.s E ) ) )
180 179 oveq1d 
 |-  ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( C x.s F ) ) )
181 129 124 96 addsubsassd 
 |-  ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( C x.s F ) ) = ( ( D x.s F ) +s ( ( C x.s E ) -s ( C x.s F ) ) ) )
182 180 181 eqtrd 
 |-  ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) = ( ( D x.s F ) +s ( ( C x.s E ) -s ( C x.s F ) ) ) )
183 182 breq2d 
 |-  ( ph -> ( ( D x.s E )  ( D x.s E )
184 124 96 subscld 
 |-  ( ph -> ( ( C x.s E ) -s ( C x.s F ) ) e. No )
185 109 129 184 sltsubadd2d 
 |-  ( ph -> ( ( ( D x.s E ) -s ( D x.s F ) )  ( D x.s E )
186 183 185 bitr4d 
 |-  ( ph -> ( ( D x.s E )  ( ( D x.s E ) -s ( D x.s F ) )
187 109 129 124 96 sltsubsub2bd 
 |-  ( ph -> ( ( ( D x.s E ) -s ( D x.s F ) )  ( ( C x.s F ) -s ( C x.s E ) )
188 186 187 bitrd 
 |-  ( ph -> ( ( D x.s E )  ( ( C x.s F ) -s ( C x.s E ) )
189 188 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( D x.s E )  ( ( C x.s F ) -s ( C x.s E ) )
190 178 189 mpbid 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
191 190 anassrs 
 |-  ( ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) /\ ( bday ` F ) e. ( bday ` E ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
192 9 adantr 
 |-  ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
193 134 191 192 mpjaodan 
 |-  ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
194 95 simp3d 
 |-  ( ph -> { ( C x.s F ) } <
195 194 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> { ( C x.s F ) } <
196 ovex 
 |-  ( C x.s F ) e. _V
197 196 snid 
 |-  ( C x.s F ) e. { ( C x.s F ) }
198 197 a1i 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F ) e. { ( C x.s F ) } )
199 simprl 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` D ) e. ( bday ` C ) )
200 bdayelon 
 |-  ( bday ` C ) e. On
201 3 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. No )
202 oldbday 
 |-  ( ( ( bday ` C ) e. On /\ D e. No ) -> ( D e. ( _Old ` ( bday ` C ) ) <-> ( bday ` D ) e. ( bday ` C ) ) )
203 200 201 202 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( D e. ( _Old ` ( bday ` C ) ) <-> ( bday ` D ) e. ( bday ` C ) ) )
204 199 203 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. ( _Old ` ( bday ` C ) ) )
205 6 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C
206 breq2 
 |-  ( x = D -> ( C  C
207 rightval 
 |-  ( _Right ` C ) = { x e. ( _Old ` ( bday ` C ) ) | C
208 206 207 elrab2 
 |-  ( D e. ( _Right ` C ) <-> ( D e. ( _Old ` ( bday ` C ) ) /\ C
209 204 205 208 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. ( _Right ` C ) )
210 simprr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` E ) e. ( bday ` F ) )
211 4 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. No )
212 48 211 50 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( E e. ( _Old ` ( bday ` F ) ) <-> ( bday ` E ) e. ( bday ` F ) ) )
213 210 212 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Old ` ( bday ` F ) ) )
214 7 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E
215 213 214 56 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) )
216 eqid 
 |-  ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) )
217 oveq1 
 |-  ( v = D -> ( v x.s F ) = ( D x.s F ) )
218 217 oveq1d 
 |-  ( v = D -> ( ( v x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s w ) ) )
219 oveq1 
 |-  ( v = D -> ( v x.s w ) = ( D x.s w ) )
220 218 219 oveq12d 
 |-  ( v = D -> ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) )
221 220 eqeq2d 
 |-  ( v = D -> ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) ) )
222 oveq2 
 |-  ( w = E -> ( C x.s w ) = ( C x.s E ) )
223 222 oveq2d 
 |-  ( w = E -> ( ( D x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s E ) ) )
224 oveq2 
 |-  ( w = E -> ( D x.s w ) = ( D x.s E ) )
225 223 224 oveq12d 
 |-  ( w = E -> ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) )
226 225 eqeq2d 
 |-  ( w = E -> ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s w ) ) -s ( D x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) )
227 221 226 rspc2ev 
 |-  ( ( D e. ( _Right ` C ) /\ E e. ( _Left ` F ) /\ ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) )
228 216 227 mp3an3 
 |-  ( ( D e. ( _Right ` C ) /\ E e. ( _Left ` F ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) )
229 209 215 228 syl2anc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) )
230 ovex 
 |-  ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. _V
231 eqeq1 
 |-  ( j = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) -> ( j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) )
232 231 2rexbidv 
 |-  ( j = ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) -> ( E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) ) )
233 230 232 elab 
 |-  ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } <-> E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) )
234 229 233 sylibr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } )
235 elun2 
 |-  ( ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. ( { i | E. t e. ( _Left ` C ) E. u e. ( _Right ` F ) i = ( ( ( t x.s F ) +s ( C x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) )
236 234 235 syl 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. ( { i | E. t e. ( _Left ` C ) E. u e. ( _Right ` F ) i = ( ( ( t x.s F ) +s ( C x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` C ) E. w e. ( _Left ` F ) j = ( ( ( v x.s F ) +s ( C x.s w ) ) -s ( v x.s w ) ) } ) )
237 195 198 236 ssltsepcd 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F )
238 129 124 addscomd 
 |-  ( ph -> ( ( D x.s F ) +s ( C x.s E ) ) = ( ( C x.s E ) +s ( D x.s F ) ) )
239 238 oveq1d 
 |-  ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( D x.s E ) ) )
240 124 129 109 addsubsassd 
 |-  ( ph -> ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( D x.s E ) ) = ( ( C x.s E ) +s ( ( D x.s F ) -s ( D x.s E ) ) ) )
241 239 240 eqtrd 
 |-  ( ph -> ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) = ( ( C x.s E ) +s ( ( D x.s F ) -s ( D x.s E ) ) ) )
242 241 breq2d 
 |-  ( ph -> ( ( C x.s F )  ( C x.s F )
243 129 109 subscld 
 |-  ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No )
244 96 124 243 sltsubadd2d 
 |-  ( ph -> ( ( ( C x.s F ) -s ( C x.s E ) )  ( C x.s F )
245 242 244 bitr4d 
 |-  ( ph -> ( ( C x.s F )  ( ( C x.s F ) -s ( C x.s E ) )
246 245 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F )  ( ( C x.s F ) -s ( C x.s E ) )
247 237 246 mpbid 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
248 247 anassrs 
 |-  ( ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) /\ ( bday ` E ) e. ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
249 123 simp2d 
 |-  ( ph -> ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
250 249 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) <
251 simprl 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` D ) e. ( bday ` C ) )
252 3 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. No )
253 200 252 202 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D e. ( _Old ` ( bday ` C ) ) <-> ( bday ` D ) e. ( bday ` C ) ) )
254 251 253 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. ( _Old ` ( bday ` C ) ) )
255 6 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C
256 254 255 208 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. ( _Right ` C ) )
257 simprr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` F ) e. ( bday ` E ) )
258 5 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. No )
259 147 258 149 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( F e. ( _Old ` ( bday ` E ) ) <-> ( bday ` F ) e. ( bday ` E ) ) )
260 257 259 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Old ` ( bday ` E ) ) )
261 7 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E
262 260 261 155 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) )
263 eqid 
 |-  ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )
264 oveq1 
 |-  ( r = D -> ( r x.s E ) = ( D x.s E ) )
265 264 oveq1d 
 |-  ( r = D -> ( ( r x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s s ) ) )
266 oveq1 
 |-  ( r = D -> ( r x.s s ) = ( D x.s s ) )
267 265 266 oveq12d 
 |-  ( r = D -> ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) )
268 267 eqeq2d 
 |-  ( r = D -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) ) )
269 oveq2 
 |-  ( s = F -> ( C x.s s ) = ( C x.s F ) )
270 269 oveq2d 
 |-  ( s = F -> ( ( D x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s F ) ) )
271 oveq2 
 |-  ( s = F -> ( D x.s s ) = ( D x.s F ) )
272 270 271 oveq12d 
 |-  ( s = F -> ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) )
273 272 eqeq2d 
 |-  ( s = F -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s s ) ) -s ( D x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) )
274 268 273 rspc2ev 
 |-  ( ( D e. ( _Right ` C ) /\ F e. ( _Right ` E ) /\ ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) )
275 263 274 mp3an3 
 |-  ( ( D e. ( _Right ` C ) /\ F e. ( _Right ` E ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) )
276 256 262 275 syl2anc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) )
277 ovex 
 |-  ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. _V
278 eqeq1 
 |-  ( h = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) -> ( h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) )
279 278 2rexbidv 
 |-  ( h = ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) -> ( E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) <-> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) ) )
280 277 279 elab 
 |-  ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } <-> E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) )
281 276 280 sylibr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } )
282 elun2 
 |-  ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) )
283 281 282 syl 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. ( { g | E. p e. ( _Left ` C ) E. q e. ( _Left ` E ) g = ( ( ( p x.s E ) +s ( C x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` C ) E. s e. ( _Right ` E ) h = ( ( ( r x.s E ) +s ( C x.s s ) ) -s ( r x.s s ) ) } ) )
284 ovex 
 |-  ( C x.s E ) e. _V
285 284 snid 
 |-  ( C x.s E ) e. { ( C x.s E ) }
286 285 a1i 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( C x.s E ) e. { ( C x.s E ) } )
287 250 283 286 ssltsepcd 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )
288 109 96 addscomd 
 |-  ( ph -> ( ( D x.s E ) +s ( C x.s F ) ) = ( ( C x.s F ) +s ( D x.s E ) ) )
289 288 oveq1d 
 |-  ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( D x.s F ) ) )
290 96 109 129 addsubsassd 
 |-  ( ph -> ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( D x.s F ) ) = ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) )
291 289 290 eqtrd 
 |-  ( ph -> ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) = ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) ) )
292 291 breq1d 
 |-  ( ph -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )  ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) )
293 109 129 subscld 
 |-  ( ph -> ( ( D x.s E ) -s ( D x.s F ) ) e. No )
294 96 293 124 sltaddsub2d 
 |-  ( ph -> ( ( ( C x.s F ) +s ( ( D x.s E ) -s ( D x.s F ) ) )  ( ( D x.s E ) -s ( D x.s F ) )
295 292 294 bitrd 
 |-  ( ph -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )  ( ( D x.s E ) -s ( D x.s F ) )
296 295 187 bitrd 
 |-  ( ph -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )  ( ( C x.s F ) -s ( C x.s E ) )
297 296 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) )  ( ( C x.s F ) -s ( C x.s E ) )
298 287 297 mpbid 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
299 298 anassrs 
 |-  ( ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) /\ ( bday ` F ) e. ( bday ` E ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
300 9 adantr 
 |-  ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
301 248 299 300 mpjaodan 
 |-  ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
302 193 301 8 mpjaodan 
 |-  ( ph -> ( ( C x.s F ) -s ( C x.s E ) )