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 elleft 
 |-  ( C e. ( _Left ` D ) <-> ( C e. ( _Old ` ( bday ` D ) ) /\ C
44 41 42 43 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C e. ( _Left ` D ) )
45 simprr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` E ) e. ( bday ` F ) )
46 bdayelon 
 |-  ( bday ` F ) e. On
47 4 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. No )
48 oldbday 
 |-  ( ( ( bday ` F ) e. On /\ E e. No ) -> ( E e. ( _Old ` ( bday ` F ) ) <-> ( bday ` E ) e. ( bday ` F ) ) )
49 46 47 48 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( E e. ( _Old ` ( bday ` F ) ) <-> ( bday ` E ) e. ( bday ` F ) ) )
50 45 49 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Old ` ( bday ` F ) ) )
51 7 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E
52 elleft 
 |-  ( E e. ( _Left ` F ) <-> ( E e. ( _Old ` ( bday ` F ) ) /\ E
53 50 51 52 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) )
54 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 ) )
55 oveq1 
 |-  ( p = C -> ( p x.s F ) = ( C x.s F ) )
56 55 oveq1d 
 |-  ( p = C -> ( ( p x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s q ) ) )
57 oveq1 
 |-  ( p = C -> ( p x.s q ) = ( C x.s q ) )
58 56 57 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 ) ) )
59 58 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 ) ) ) )
60 oveq2 
 |-  ( q = E -> ( D x.s q ) = ( D x.s E ) )
61 60 oveq2d 
 |-  ( q = E -> ( ( C x.s F ) +s ( D x.s q ) ) = ( ( C x.s F ) +s ( D x.s E ) ) )
62 oveq2 
 |-  ( q = E -> ( C x.s q ) = ( C x.s E ) )
63 61 62 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 ) ) )
64 63 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 ) ) ) )
65 59 64 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 ) ) )
66 54 65 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 ) ) )
67 44 53 66 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 ) ) )
68 ovex 
 |-  ( ( ( C x.s F ) +s ( D x.s E ) ) -s ( C x.s E ) ) e. _V
69 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 ) ) ) )
70 69 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 ) ) ) )
71 68 70 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 ) ) )
72 67 71 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 ) ) } )
73 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 ) ) } ) )
74 72 73 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 ) ) } ) )
75 ovex 
 |-  ( D x.s F ) e. _V
76 75 snid 
 |-  ( D x.s F ) e. { ( D x.s F ) }
77 76 a1i 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( D x.s F ) e. { ( D x.s F ) } )
78 35 74 77 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 ) )
79 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. (/) )
80 un0 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) )
81 79 80 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 ) )
82 ssun1 
 |-  ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
83 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 ) ) ) )
84 82 83 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 ) ) ) )
85 84 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 ) ) ) ) )
86 81 85 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 ) ) ) ) )
87 86 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 ) ) ) ) ) )
88 87 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 ) )
89 88 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 ) )
90 1 89 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 ) )
91 90 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 ) ) } ) <
92 91 simp1d 
 |-  ( ph -> ( C x.s F ) e. No )
93 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. (/) )
94 un0 
 |-  ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) )
95 93 94 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 ) )
96 ssun2 
 |-  ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
97 96 83 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 ) ) ) )
98 97 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 ) ) ) ) )
99 95 98 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 ) ) ) ) )
100 99 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 ) ) ) ) ) )
101 100 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 ) )
102 101 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 ) )
103 1 102 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 ) )
104 103 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 ) ) } ) <
105 104 simp1d 
 |-  ( ph -> ( D x.s E ) e. No )
106 92 105 addscomd 
 |-  ( ph -> ( ( C x.s F ) +s ( D x.s E ) ) = ( ( D x.s E ) +s ( C x.s F ) ) )
107 106 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 ) ) )
108 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. (/) )
109 un0 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) )
110 108 109 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 ) )
111 ssun1 
 |-  ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
112 111 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 ) ) ) )
113 112 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 ) ) ) ) )
114 110 113 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 ) ) ) ) )
115 114 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 ) ) ) ) ) )
116 115 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 ) )
117 116 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 ) )
118 1 117 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 ) )
119 118 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 ) ) } ) <
120 119 simp1d 
 |-  ( ph -> ( C x.s E ) e. No )
121 105 92 120 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 ) ) ) )
122 107 121 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 ) ) ) )
123 122 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 ) ) )
124 92 120 subscld 
 |-  ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No )
125 33 simp1d 
 |-  ( ph -> ( D x.s F ) e. No )
126 105 124 125 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 ) )
127 123 126 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 ) )
128 127 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 ) )
129 78 128 mpbid 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
130 129 anassrs 
 |-  ( ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) /\ ( bday ` E ) e. ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
131 104 simp3d 
 |-  ( ph -> { ( D x.s E ) } <
132 131 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> { ( D x.s E ) } <
133 ovex 
 |-  ( D x.s E ) e. _V
134 133 snid 
 |-  ( D x.s E ) e. { ( D x.s E ) }
135 134 a1i 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E ) e. { ( D x.s E ) } )
136 simprl 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` C ) e. ( bday ` D ) )
137 2 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. No )
138 37 137 39 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( C e. ( _Old ` ( bday ` D ) ) <-> ( bday ` C ) e. ( bday ` D ) ) )
139 136 138 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. ( _Old ` ( bday ` D ) ) )
140 6 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C
141 139 140 43 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C e. ( _Left ` D ) )
142 simprr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` F ) e. ( bday ` E ) )
143 bdayelon 
 |-  ( bday ` E ) e. On
144 5 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. No )
145 oldbday 
 |-  ( ( ( bday ` E ) e. On /\ F e. No ) -> ( F e. ( _Old ` ( bday ` E ) ) <-> ( bday ` F ) e. ( bday ` E ) ) )
146 143 144 145 sylancr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( F e. ( _Old ` ( bday ` E ) ) <-> ( bday ` F ) e. ( bday ` E ) ) )
147 142 146 mpbird 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Old ` ( bday ` E ) ) )
148 7 adantr 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E
149 elright 
 |-  ( F e. ( _Right ` E ) <-> ( F e. ( _Old ` ( bday ` E ) ) /\ E
150 147 148 149 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) )
151 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 ) )
152 oveq1 
 |-  ( t = C -> ( t x.s E ) = ( C x.s E ) )
153 152 oveq1d 
 |-  ( t = C -> ( ( t x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s u ) ) )
154 oveq1 
 |-  ( t = C -> ( t x.s u ) = ( C x.s u ) )
155 153 154 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 ) ) )
156 155 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 ) ) ) )
157 oveq2 
 |-  ( u = F -> ( D x.s u ) = ( D x.s F ) )
158 157 oveq2d 
 |-  ( u = F -> ( ( C x.s E ) +s ( D x.s u ) ) = ( ( C x.s E ) +s ( D x.s F ) ) )
159 oveq2 
 |-  ( u = F -> ( C x.s u ) = ( C x.s F ) )
160 158 159 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 ) ) )
161 160 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 ) ) ) )
162 156 161 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 ) ) )
163 151 162 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 ) ) )
164 141 150 163 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 ) ) )
165 ovex 
 |-  ( ( ( C x.s E ) +s ( D x.s F ) ) -s ( C x.s F ) ) e. _V
166 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 ) ) ) )
167 166 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 ) ) ) )
168 165 167 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 ) ) )
169 164 168 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 ) ) } )
170 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 ) ) } ) )
171 169 170 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 ) ) } ) )
172 132 135 171 ssltsepcd 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D x.s E )
173 120 125 addscomd 
 |-  ( ph -> ( ( C x.s E ) +s ( D x.s F ) ) = ( ( D x.s F ) +s ( C x.s E ) ) )
174 173 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 ) ) )
175 125 120 92 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 ) ) ) )
176 174 175 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 ) ) ) )
177 176 breq2d 
 |-  ( ph -> ( ( D x.s E )  ( D x.s E )
178 120 92 subscld 
 |-  ( ph -> ( ( C x.s E ) -s ( C x.s F ) ) e. No )
179 105 125 178 sltsubadd2d 
 |-  ( ph -> ( ( ( D x.s E ) -s ( D x.s F ) )  ( D x.s E )
180 177 179 bitr4d 
 |-  ( ph -> ( ( D x.s E )  ( ( D x.s E ) -s ( D x.s F ) )
181 105 125 120 92 sltsubsub2bd 
 |-  ( ph -> ( ( ( D x.s E ) -s ( D x.s F ) )  ( ( C x.s F ) -s ( C x.s E ) )
182 180 181 bitrd 
 |-  ( ph -> ( ( D x.s E )  ( ( C x.s F ) -s ( C x.s E ) )
183 182 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 ) )
184 172 183 mpbid 
 |-  ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
185 184 anassrs 
 |-  ( ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) /\ ( bday ` F ) e. ( bday ` E ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
186 9 adantr 
 |-  ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
187 130 185 186 mpjaodan 
 |-  ( ( ph /\ ( bday ` C ) e. ( bday ` D ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
188 91 simp3d 
 |-  ( ph -> { ( C x.s F ) } <
189 188 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> { ( C x.s F ) } <
190 ovex 
 |-  ( C x.s F ) e. _V
191 190 snid 
 |-  ( C x.s F ) e. { ( C x.s F ) }
192 191 a1i 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F ) e. { ( C x.s F ) } )
193 simprl 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` D ) e. ( bday ` C ) )
194 bdayelon 
 |-  ( bday ` C ) e. On
195 3 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. No )
196 oldbday 
 |-  ( ( ( bday ` C ) e. On /\ D e. No ) -> ( D e. ( _Old ` ( bday ` C ) ) <-> ( bday ` D ) e. ( bday ` C ) ) )
197 194 195 196 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( D e. ( _Old ` ( bday ` C ) ) <-> ( bday ` D ) e. ( bday ` C ) ) )
198 193 197 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. ( _Old ` ( bday ` C ) ) )
199 6 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> C
200 elright 
 |-  ( D e. ( _Right ` C ) <-> ( D e. ( _Old ` ( bday ` C ) ) /\ C
201 198 199 200 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> D e. ( _Right ` C ) )
202 simprr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( bday ` E ) e. ( bday ` F ) )
203 4 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. No )
204 46 203 48 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( E e. ( _Old ` ( bday ` F ) ) <-> ( bday ` E ) e. ( bday ` F ) ) )
205 202 204 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Old ` ( bday ` F ) ) )
206 7 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E
207 205 206 52 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> E e. ( _Left ` F ) )
208 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 ) )
209 oveq1 
 |-  ( v = D -> ( v x.s F ) = ( D x.s F ) )
210 209 oveq1d 
 |-  ( v = D -> ( ( v x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s w ) ) )
211 oveq1 
 |-  ( v = D -> ( v x.s w ) = ( D x.s w ) )
212 210 211 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 ) ) )
213 212 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 ) ) ) )
214 oveq2 
 |-  ( w = E -> ( C x.s w ) = ( C x.s E ) )
215 214 oveq2d 
 |-  ( w = E -> ( ( D x.s F ) +s ( C x.s w ) ) = ( ( D x.s F ) +s ( C x.s E ) ) )
216 oveq2 
 |-  ( w = E -> ( D x.s w ) = ( D x.s E ) )
217 215 216 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 ) ) )
218 217 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 ) ) ) )
219 213 218 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 ) ) )
220 208 219 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 ) ) )
221 201 207 220 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 ) ) )
222 ovex 
 |-  ( ( ( D x.s F ) +s ( C x.s E ) ) -s ( D x.s E ) ) e. _V
223 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 ) ) ) )
224 223 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 ) ) ) )
225 222 224 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 ) ) )
226 221 225 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 ) ) } )
227 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 ) ) } ) )
228 226 227 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 ) ) } ) )
229 189 192 228 ssltsepcd 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( C x.s F )
230 125 120 addscomd 
 |-  ( ph -> ( ( D x.s F ) +s ( C x.s E ) ) = ( ( C x.s E ) +s ( D x.s F ) ) )
231 230 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 ) ) )
232 120 125 105 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 ) ) ) )
233 231 232 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 ) ) ) )
234 233 breq2d 
 |-  ( ph -> ( ( C x.s F )  ( C x.s F )
235 125 105 subscld 
 |-  ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No )
236 92 120 235 sltsubadd2d 
 |-  ( ph -> ( ( ( C x.s F ) -s ( C x.s E ) )  ( C x.s F )
237 234 236 bitr4d 
 |-  ( ph -> ( ( C x.s F )  ( ( C x.s F ) -s ( C x.s E ) )
238 237 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 ) )
239 229 238 mpbid 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` E ) e. ( bday ` F ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
240 239 anassrs 
 |-  ( ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) /\ ( bday ` E ) e. ( bday ` F ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
241 119 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 ) ) } ) <
242 241 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 ) ) } ) <
243 simprl 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` D ) e. ( bday ` C ) )
244 3 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. No )
245 194 244 196 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( D e. ( _Old ` ( bday ` C ) ) <-> ( bday ` D ) e. ( bday ` C ) ) )
246 243 245 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. ( _Old ` ( bday ` C ) ) )
247 6 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> C
248 246 247 200 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> D e. ( _Right ` C ) )
249 simprr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( bday ` F ) e. ( bday ` E ) )
250 5 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. No )
251 143 250 145 sylancr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( F e. ( _Old ` ( bday ` E ) ) <-> ( bday ` F ) e. ( bday ` E ) ) )
252 249 251 mpbird 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Old ` ( bday ` E ) ) )
253 7 adantr 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> E
254 252 253 149 sylanbrc 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> F e. ( _Right ` E ) )
255 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 ) )
256 oveq1 
 |-  ( r = D -> ( r x.s E ) = ( D x.s E ) )
257 256 oveq1d 
 |-  ( r = D -> ( ( r x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s s ) ) )
258 oveq1 
 |-  ( r = D -> ( r x.s s ) = ( D x.s s ) )
259 257 258 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 ) ) )
260 259 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 ) ) ) )
261 oveq2 
 |-  ( s = F -> ( C x.s s ) = ( C x.s F ) )
262 261 oveq2d 
 |-  ( s = F -> ( ( D x.s E ) +s ( C x.s s ) ) = ( ( D x.s E ) +s ( C x.s F ) ) )
263 oveq2 
 |-  ( s = F -> ( D x.s s ) = ( D x.s F ) )
264 262 263 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 ) ) )
265 264 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 ) ) ) )
266 260 265 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 ) ) )
267 255 266 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 ) ) )
268 248 254 267 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 ) ) )
269 ovex 
 |-  ( ( ( D x.s E ) +s ( C x.s F ) ) -s ( D x.s F ) ) e. _V
270 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 ) ) ) )
271 270 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 ) ) ) )
272 269 271 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 ) ) )
273 268 272 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 ) ) } )
274 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 ) ) } ) )
275 273 274 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 ) ) } ) )
276 ovex 
 |-  ( C x.s E ) e. _V
277 276 snid 
 |-  ( C x.s E ) e. { ( C x.s E ) }
278 277 a1i 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( C x.s E ) e. { ( C x.s E ) } )
279 242 275 278 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 ) )
280 105 92 addscomd 
 |-  ( ph -> ( ( D x.s E ) +s ( C x.s F ) ) = ( ( C x.s F ) +s ( D x.s E ) ) )
281 280 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 ) ) )
282 92 105 125 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 ) ) ) )
283 281 282 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 ) ) ) )
284 283 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 ) ) )
285 105 125 subscld 
 |-  ( ph -> ( ( D x.s E ) -s ( D x.s F ) ) e. No )
286 92 285 120 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 ) )
287 284 286 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 ) )
288 287 181 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 ) )
289 288 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 ) )
290 279 289 mpbid 
 |-  ( ( ph /\ ( ( bday ` D ) e. ( bday ` C ) /\ ( bday ` F ) e. ( bday ` E ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
291 290 anassrs 
 |-  ( ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) /\ ( bday ` F ) e. ( bday ` E ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
292 9 adantr 
 |-  ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
293 240 291 292 mpjaodan 
 |-  ( ( ph /\ ( bday ` D ) e. ( bday ` C ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
294 187 293 8 mpjaodan 
 |-  ( ph -> ( ( C x.s F ) -s ( C x.s E ) )