Metamath Proof Explorer

Theorem mulsprop

Description: Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of Gonshor p. 17. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Assertion mulsprop 
|- ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s F ) -s ( C x.s E ) )

Proof

Step Hyp Ref Expression
1 bdayelon 
 |-  ( bday ` A ) e. On
2 bdayelon 
 |-  ( bday ` B ) e. On
3 naddcl 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) +no ( bday ` B ) ) e. On )
4 1 2 3 mp2an 
 |-  ( ( bday ` A ) +no ( bday ` B ) ) e. On
5 bdayelon 
 |-  ( bday ` C ) e. On
6 bdayelon 
 |-  ( bday ` E ) e. On
7 naddcl 
 |-  ( ( ( bday ` C ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` C ) +no ( bday ` E ) ) e. On )
8 5 6 7 mp2an 
 |-  ( ( bday ` C ) +no ( bday ` E ) ) e. On
9 bdayelon 
 |-  ( bday ` D ) e. On
10 bdayelon 
 |-  ( bday ` F ) e. On
11 naddcl 
 |-  ( ( ( bday ` D ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` D ) +no ( bday ` F ) ) e. On )
12 9 10 11 mp2an 
 |-  ( ( bday ` D ) +no ( bday ` F ) ) e. On
13 8 12 onun2i 
 |-  ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) e. On
14 naddcl 
 |-  ( ( ( bday ` C ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` C ) +no ( bday ` F ) ) e. On )
15 5 10 14 mp2an 
 |-  ( ( bday ` C ) +no ( bday ` F ) ) e. On
16 naddcl 
 |-  ( ( ( bday ` D ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` D ) +no ( bday ` E ) ) e. On )
17 9 6 16 mp2an 
 |-  ( ( bday ` D ) +no ( bday ` E ) ) e. On
18 15 17 onun2i 
 |-  ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) e. On
19 13 18 onun2i 
 |-  ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) e. On
20 4 19 onun2i 
 |-  ( ( ( 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. On
21 risset 
 |-  ( ( ( ( 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. On <-> E. x e. On x = ( ( ( 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 ) ) ) ) ) )
22 20 21 mpbi 
 |-  E. x e. On x = ( ( ( 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 ) ) ) ) )
23 fveq2 
 |-  ( a = g -> ( bday ` a ) = ( bday ` g ) )
24 23 oveq1d 
 |-  ( a = g -> ( ( bday ` a ) +no ( bday ` b ) ) = ( ( bday ` g ) +no ( bday ` b ) ) )
25 24 uneq1d 
 |-  ( a = g -> ( ( ( 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 ) ) ) ) ) = ( ( ( bday ` g ) +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 ) ) ) ) ) )
26 25 eqeq2d 
 |-  ( a = g -> ( x = ( ( ( 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 ) ) ) ) ) <-> x = ( ( ( bday ` g ) +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 oveq1 
 |-  ( a = g -> ( a x.s b ) = ( g x.s b ) )
28 27 eleq1d 
 |-  ( a = g -> ( ( a x.s b ) e. No <-> ( g x.s b ) e. No ) )
29 28 anbi1d 
 |-  ( a = g -> ( ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( g x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
30 26 29 imbi12d 
 |-  ( a = g -> ( ( x = ( ( ( 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 ) )  ( x = ( ( ( bday ` g ) +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 ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
31 fveq2 
 |-  ( b = h -> ( bday ` b ) = ( bday ` h ) )
32 31 oveq2d 
 |-  ( b = h -> ( ( bday ` g ) +no ( bday ` b ) ) = ( ( bday ` g ) +no ( bday ` h ) ) )
33 32 uneq1d 
 |-  ( b = h -> ( ( ( bday ` g ) +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 ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) )
34 33 eqeq2d 
 |-  ( b = h -> ( x = ( ( ( bday ` g ) +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 ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) )
35 oveq2 
 |-  ( b = h -> ( g x.s b ) = ( g x.s h ) )
36 35 eleq1d 
 |-  ( b = h -> ( ( g x.s b ) e. No <-> ( g x.s h ) e. No ) )
37 36 anbi1d 
 |-  ( b = h -> ( ( ( g x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( g x.s h ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
38 34 37 imbi12d 
 |-  ( b = h -> ( ( x = ( ( ( bday ` g ) +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 ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
39 fveq2 
 |-  ( c = i -> ( bday ` c ) = ( bday ` i ) )
40 39 oveq1d 
 |-  ( c = i -> ( ( bday ` c ) +no ( bday ` e ) ) = ( ( bday ` i ) +no ( bday ` e ) ) )
41 40 uneq1d 
 |-  ( c = i -> ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) )
42 39 oveq1d 
 |-  ( c = i -> ( ( bday ` c ) +no ( bday ` f ) ) = ( ( bday ` i ) +no ( bday ` f ) ) )
43 42 uneq1d 
 |-  ( c = i -> ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) )
44 41 43 uneq12d 
 |-  ( c = i -> ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) )
45 44 uneq2d 
 |-  ( c = i -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) )
46 45 eqeq2d 
 |-  ( c = i -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) )
47 breq1 
 |-  ( c = i -> ( c  i
48 47 anbi1d 
 |-  ( c = i -> ( ( c  ( i
49 oveq1 
 |-  ( c = i -> ( c x.s f ) = ( i x.s f ) )
50 oveq1 
 |-  ( c = i -> ( c x.s e ) = ( i x.s e ) )
51 49 50 oveq12d 
 |-  ( c = i -> ( ( c x.s f ) -s ( c x.s e ) ) = ( ( i x.s f ) -s ( i x.s e ) ) )
52 51 breq1d 
 |-  ( c = i -> ( ( ( c x.s f ) -s ( c x.s e ) )  ( ( i x.s f ) -s ( i x.s e ) )
53 48 52 imbi12d 
 |-  ( c = i -> ( ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( i  ( ( i x.s f ) -s ( i x.s e ) )
54 53 anbi2d 
 |-  ( c = i -> ( ( ( g x.s h ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )
55 46 54 imbi12d 
 |-  ( c = i -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )
56 fveq2 
 |-  ( d = j -> ( bday ` d ) = ( bday ` j ) )
57 56 oveq1d 
 |-  ( d = j -> ( ( bday ` d ) +no ( bday ` f ) ) = ( ( bday ` j ) +no ( bday ` f ) ) )
58 57 uneq2d 
 |-  ( d = j -> ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) )
59 56 oveq1d 
 |-  ( d = j -> ( ( bday ` d ) +no ( bday ` e ) ) = ( ( bday ` j ) +no ( bday ` e ) ) )
60 59 uneq2d 
 |-  ( d = j -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) )
61 58 60 uneq12d 
 |-  ( d = j -> ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) )
62 61 uneq2d 
 |-  ( d = j -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) )
63 62 eqeq2d 
 |-  ( d = j -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) ) )
64 breq2 
 |-  ( d = j -> ( i  i
65 64 anbi1d 
 |-  ( d = j -> ( ( i  ( i
66 oveq1 
 |-  ( d = j -> ( d x.s f ) = ( j x.s f ) )
67 oveq1 
 |-  ( d = j -> ( d x.s e ) = ( j x.s e ) )
68 66 67 oveq12d 
 |-  ( d = j -> ( ( d x.s f ) -s ( d x.s e ) ) = ( ( j x.s f ) -s ( j x.s e ) ) )
69 68 breq2d 
 |-  ( d = j -> ( ( ( i x.s f ) -s ( i x.s e ) )  ( ( i x.s f ) -s ( i x.s e ) )
70 65 69 imbi12d 
 |-  ( d = j -> ( ( ( i  ( ( i x.s f ) -s ( i x.s e ) )  ( ( i  ( ( i x.s f ) -s ( i x.s e ) )
71 70 anbi2d 
 |-  ( d = j -> ( ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )  ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )
72 63 71 imbi12d 
 |-  ( d = j -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )
73 fveq2 
 |-  ( e = k -> ( bday ` e ) = ( bday ` k ) )
74 73 oveq2d 
 |-  ( e = k -> ( ( bday ` i ) +no ( bday ` e ) ) = ( ( bday ` i ) +no ( bday ` k ) ) )
75 74 uneq1d 
 |-  ( e = k -> ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) )
76 73 oveq2d 
 |-  ( e = k -> ( ( bday ` j ) +no ( bday ` e ) ) = ( ( bday ` j ) +no ( bday ` k ) ) )
77 76 uneq2d 
 |-  ( e = k -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) )
78 75 77 uneq12d 
 |-  ( e = k -> ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) )
79 78 uneq2d 
 |-  ( e = k -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) )
80 79 eqeq2d 
 |-  ( e = k -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) )
81 breq1 
 |-  ( e = k -> ( e  k
82 81 anbi2d 
 |-  ( e = k -> ( ( i  ( i
83 oveq2 
 |-  ( e = k -> ( i x.s e ) = ( i x.s k ) )
84 83 oveq2d 
 |-  ( e = k -> ( ( i x.s f ) -s ( i x.s e ) ) = ( ( i x.s f ) -s ( i x.s k ) ) )
85 oveq2 
 |-  ( e = k -> ( j x.s e ) = ( j x.s k ) )
86 85 oveq2d 
 |-  ( e = k -> ( ( j x.s f ) -s ( j x.s e ) ) = ( ( j x.s f ) -s ( j x.s k ) ) )
87 84 86 breq12d 
 |-  ( e = k -> ( ( ( i x.s f ) -s ( i x.s e ) )  ( ( i x.s f ) -s ( i x.s k ) )
88 82 87 imbi12d 
 |-  ( e = k -> ( ( ( i  ( ( i x.s f ) -s ( i x.s e ) )  ( ( i  ( ( i x.s f ) -s ( i x.s k ) )
89 88 anbi2d 
 |-  ( e = k -> ( ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )  ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s k ) )
90 80 89 imbi12d 
 |-  ( e = k -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s e ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s k ) )
91 fveq2 
 |-  ( f = l -> ( bday ` f ) = ( bday ` l ) )
92 91 oveq2d 
 |-  ( f = l -> ( ( bday ` j ) +no ( bday ` f ) ) = ( ( bday ` j ) +no ( bday ` l ) ) )
93 92 uneq2d 
 |-  ( f = l -> ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) )
94 91 oveq2d 
 |-  ( f = l -> ( ( bday ` i ) +no ( bday ` f ) ) = ( ( bday ` i ) +no ( bday ` l ) ) )
95 94 uneq1d 
 |-  ( f = l -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) )
96 93 95 uneq12d 
 |-  ( f = l -> ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) )
97 96 uneq2d 
 |-  ( f = l -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) )
98 97 eqeq2d 
 |-  ( f = l -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) )
99 breq2 
 |-  ( f = l -> ( k  k
100 99 anbi2d 
 |-  ( f = l -> ( ( i  ( i
101 oveq2 
 |-  ( f = l -> ( i x.s f ) = ( i x.s l ) )
102 101 oveq1d 
 |-  ( f = l -> ( ( i x.s f ) -s ( i x.s k ) ) = ( ( i x.s l ) -s ( i x.s k ) ) )
103 oveq2 
 |-  ( f = l -> ( j x.s f ) = ( j x.s l ) )
104 103 oveq1d 
 |-  ( f = l -> ( ( j x.s f ) -s ( j x.s k ) ) = ( ( j x.s l ) -s ( j x.s k ) ) )
105 102 104 breq12d 
 |-  ( f = l -> ( ( ( i x.s f ) -s ( i x.s k ) )  ( ( i x.s l ) -s ( i x.s k ) )
106 100 105 imbi12d 
 |-  ( f = l -> ( ( ( i  ( ( i x.s f ) -s ( i x.s k ) )  ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
107 106 anbi2d 
 |-  ( f = l -> ( ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s k ) )  ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
108 98 107 imbi12d 
 |-  ( f = l -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s f ) -s ( i x.s k ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
109 30 38 55 72 90 108 cbvral6vw 
 |-  ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( x = ( ( ( 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. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
110 eqeq1 
 |-  ( x = y -> ( x = ( ( ( 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 ) ) ) ) ) <-> y = ( ( ( 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 ) ) ) ) ) ) )
111 110 imbi1d 
 |-  ( x = y -> ( ( x = ( ( ( 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 ) )  ( y = ( ( ( 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 ) )
112 111 6ralbidv 
 |-  ( x = y -> ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( x = ( ( ( 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 ( y = ( ( ( 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 ) )
113 109 112 bitr3id 
 |-  ( x = y -> ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )
114 raleq 
 |-  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )
115 ralrot3 
 |-  ( A. a e. No A. b e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )
116 ralrot3 
 |-  ( A. c e. No A. d e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( 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. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )
117 ralrot3 
 |-  ( A. e e. No A. f e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( 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. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( 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 ) )
118 r19.23v 
 |-  ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( 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 ) )  ( E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( 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 ) )
119 risset 
 |-  ( ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( 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 imbi1i 
 |-  ( ( ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( 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 ) )
121 118 120 bitr4i 
 |-  ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
122 121 2ralbii 
 |-  ( A. e e. No A. f e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( 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. 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
123 117 122 bitr3i 
 |-  ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( 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. 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
124 123 2ralbii 
 |-  ( A. c e. No A. d e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( 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. 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
125 116 124 bitr3i 
 |-  ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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. 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
126 125 2ralbii 
 |-  ( A. a e. No A. b e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
127 115 126 bitr3i 
 |-  ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
128 114 127 bitrdi 
 |-  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
129 simpl 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
130 simprl1 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  g e. No )
131 simprl2 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  h e. No )
132 129 130 131 mulsproplem11 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( g x.s h ) e. No )
133 129 adantr 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )
134 simprl3 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  i e. No )
135 134 adantr 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  i e. No )
136 simprr1 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  j e. No )
137 136 adantr 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  j e. No )
138 simprr2 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  k e. No )
139 138 adantr 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  k e. No )
140 simprr3 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  l e. No )
141 140 adantr 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  l e. No )
142 simprl 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  i
143 simprr 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  k
144 133 135 137 139 141 142 143 mulsproplem14 
 |-  ( ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( i x.s l ) -s ( i x.s k ) )
145 144 ex 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
146 132 145 jca 
 |-  ( ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
147 146 ex 
 |-  ( 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 ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c  ( ( c x.s f ) -s ( c x.s e ) )  ( ( ( g e. No /\ h e. No /\ i e. No ) /\ ( j e. No /\ k e. No /\ l e. No ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
148 128 147 biimtrdi 
 |-  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )  ( ( ( g e. No /\ h e. No /\ i e. No ) /\ ( j e. No /\ k e. No /\ l e. No ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
149 148 impd 
 |-  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )  ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
150 149 com12 
 |-  ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
151 150 anassrs 
 |-  ( ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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 ) )  ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
152 151 ralrimivvva 
 |-  ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
153 152 ralrimivvva 
 |-  ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
154 153 a1i 
 |-  ( x e. On -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( 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. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
155 113 154 tfis2 
 |-  ( x e. On -> A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
156 fveq2 
 |-  ( g = A -> ( bday ` g ) = ( bday ` A ) )
157 156 oveq1d 
 |-  ( g = A -> ( ( bday ` g ) +no ( bday ` h ) ) = ( ( bday ` A ) +no ( bday ` h ) ) )
158 157 uneq1d 
 |-  ( g = A -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) )
159 158 eqeq2d 
 |-  ( g = A -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) )
160 oveq1 
 |-  ( g = A -> ( g x.s h ) = ( A x.s h ) )
161 160 eleq1d 
 |-  ( g = A -> ( ( g x.s h ) e. No <-> ( A x.s h ) e. No ) )
162 161 anbi1d 
 |-  ( g = A -> ( ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( ( A x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
163 159 162 imbi12d 
 |-  ( g = A -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
164 fveq2 
 |-  ( h = B -> ( bday ` h ) = ( bday ` B ) )
165 164 oveq2d 
 |-  ( h = B -> ( ( bday ` A ) +no ( bday ` h ) ) = ( ( bday ` A ) +no ( bday ` B ) ) )
166 165 uneq1d 
 |-  ( h = B -> ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) )
167 166 eqeq2d 
 |-  ( h = B -> ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) )
168 oveq2 
 |-  ( h = B -> ( A x.s h ) = ( A x.s B ) )
169 168 eleq1d 
 |-  ( h = B -> ( ( A x.s h ) e. No <-> ( A x.s B ) e. No ) )
170 169 anbi1d 
 |-  ( h = B -> ( ( ( A x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( ( A x.s B ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
171 167 170 imbi12d 
 |-  ( h = B -> ( ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )
172 fveq2 
 |-  ( i = C -> ( bday ` i ) = ( bday ` C ) )
173 172 oveq1d 
 |-  ( i = C -> ( ( bday ` i ) +no ( bday ` k ) ) = ( ( bday ` C ) +no ( bday ` k ) ) )
174 173 uneq1d 
 |-  ( i = C -> ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) )
175 172 oveq1d 
 |-  ( i = C -> ( ( bday ` i ) +no ( bday ` l ) ) = ( ( bday ` C ) +no ( bday ` l ) ) )
176 175 uneq1d 
 |-  ( i = C -> ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) )
177 174 176 uneq12d 
 |-  ( i = C -> ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) )
178 177 uneq2d 
 |-  ( i = C -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) )
179 178 eqeq2d 
 |-  ( i = C -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) )
180 breq1 
 |-  ( i = C -> ( i  C
181 180 anbi1d 
 |-  ( i = C -> ( ( i  ( C
182 oveq1 
 |-  ( i = C -> ( i x.s l ) = ( C x.s l ) )
183 oveq1 
 |-  ( i = C -> ( i x.s k ) = ( C x.s k ) )
184 182 183 oveq12d 
 |-  ( i = C -> ( ( i x.s l ) -s ( i x.s k ) ) = ( ( C x.s l ) -s ( C x.s k ) ) )
185 184 breq1d 
 |-  ( i = C -> ( ( ( i x.s l ) -s ( i x.s k ) )  ( ( C x.s l ) -s ( C x.s k ) )
186 181 185 imbi12d 
 |-  ( i = C -> ( ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( ( C  ( ( C x.s l ) -s ( C x.s k ) )
187 186 anbi2d 
 |-  ( i = C -> ( ( ( A x.s B ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )
188 179 187 imbi12d 
 |-  ( i = C -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )
189 fveq2 
 |-  ( j = D -> ( bday ` j ) = ( bday ` D ) )
190 189 oveq1d 
 |-  ( j = D -> ( ( bday ` j ) +no ( bday ` l ) ) = ( ( bday ` D ) +no ( bday ` l ) ) )
191 190 uneq2d 
 |-  ( j = D -> ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) )
192 189 oveq1d 
 |-  ( j = D -> ( ( bday ` j ) +no ( bday ` k ) ) = ( ( bday ` D ) +no ( bday ` k ) ) )
193 192 uneq2d 
 |-  ( j = D -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) )
194 191 193 uneq12d 
 |-  ( j = D -> ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) )
195 194 uneq2d 
 |-  ( j = D -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) )
196 195 eqeq2d 
 |-  ( j = D -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) ) )
197 breq2 
 |-  ( j = D -> ( C  C
198 197 anbi1d 
 |-  ( j = D -> ( ( C  ( C
199 oveq1 
 |-  ( j = D -> ( j x.s l ) = ( D x.s l ) )
200 oveq1 
 |-  ( j = D -> ( j x.s k ) = ( D x.s k ) )
201 199 200 oveq12d 
 |-  ( j = D -> ( ( j x.s l ) -s ( j x.s k ) ) = ( ( D x.s l ) -s ( D x.s k ) ) )
202 201 breq2d 
 |-  ( j = D -> ( ( ( C x.s l ) -s ( C x.s k ) )  ( ( C x.s l ) -s ( C x.s k ) )
203 198 202 imbi12d 
 |-  ( j = D -> ( ( ( C  ( ( C x.s l ) -s ( C x.s k ) )  ( ( C  ( ( C x.s l ) -s ( C x.s k ) )
204 203 anbi2d 
 |-  ( j = D -> ( ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )  ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )
205 196 204 imbi12d 
 |-  ( j = D -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )  ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )
206 fveq2 
 |-  ( k = E -> ( bday ` k ) = ( bday ` E ) )
207 206 oveq2d 
 |-  ( k = E -> ( ( bday ` C ) +no ( bday ` k ) ) = ( ( bday ` C ) +no ( bday ` E ) ) )
208 207 uneq1d 
 |-  ( k = E -> ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) )
209 206 oveq2d 
 |-  ( k = E -> ( ( bday ` D ) +no ( bday ` k ) ) = ( ( bday ` D ) +no ( bday ` E ) ) )
210 209 uneq2d 
 |-  ( k = E -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
211 208 210 uneq12d 
 |-  ( k = E -> ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) )
212 211 uneq2d 
 |-  ( k = E -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) )
213 212 eqeq2d 
 |-  ( k = E -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) )
214 breq1 
 |-  ( k = E -> ( k  E
215 214 anbi2d 
 |-  ( k = E -> ( ( C  ( C
216 oveq2 
 |-  ( k = E -> ( C x.s k ) = ( C x.s E ) )
217 216 oveq2d 
 |-  ( k = E -> ( ( C x.s l ) -s ( C x.s k ) ) = ( ( C x.s l ) -s ( C x.s E ) ) )
218 oveq2 
 |-  ( k = E -> ( D x.s k ) = ( D x.s E ) )
219 218 oveq2d 
 |-  ( k = E -> ( ( D x.s l ) -s ( D x.s k ) ) = ( ( D x.s l ) -s ( D x.s E ) ) )
220 217 219 breq12d 
 |-  ( k = E -> ( ( ( C x.s l ) -s ( C x.s k ) )  ( ( C x.s l ) -s ( C x.s E ) )
221 215 220 imbi12d 
 |-  ( k = E -> ( ( ( C  ( ( C x.s l ) -s ( C x.s k ) )  ( ( C  ( ( C x.s l ) -s ( C x.s E ) )
222 221 anbi2d 
 |-  ( k = E -> ( ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )  ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s E ) )
223 213 222 imbi12d 
 |-  ( k = E -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s k ) )  ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s E ) )
224 fveq2 
 |-  ( l = F -> ( bday ` l ) = ( bday ` F ) )
225 224 oveq2d 
 |-  ( l = F -> ( ( bday ` D ) +no ( bday ` l ) ) = ( ( bday ` D ) +no ( bday ` F ) ) )
226 225 uneq2d 
 |-  ( l = F -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) )
227 224 oveq2d 
 |-  ( l = F -> ( ( bday ` C ) +no ( bday ` l ) ) = ( ( bday ` C ) +no ( bday ` F ) ) )
228 227 uneq1d 
 |-  ( l = F -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
229 226 228 uneq12d 
 |-  ( l = F -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) )
230 229 uneq2d 
 |-  ( l = F -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` 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 ) ) ) ) ) )
231 230 eqeq2d 
 |-  ( l = F -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) <-> x = ( ( ( 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 ) ) ) ) ) ) )
232 breq2 
 |-  ( l = F -> ( E  E
233 232 anbi2d 
 |-  ( l = F -> ( ( C  ( C
234 oveq2 
 |-  ( l = F -> ( C x.s l ) = ( C x.s F ) )
235 234 oveq1d 
 |-  ( l = F -> ( ( C x.s l ) -s ( C x.s E ) ) = ( ( C x.s F ) -s ( C x.s E ) ) )
236 oveq2 
 |-  ( l = F -> ( D x.s l ) = ( D x.s F ) )
237 236 oveq1d 
 |-  ( l = F -> ( ( D x.s l ) -s ( D x.s E ) ) = ( ( D x.s F ) -s ( D x.s E ) ) )
238 235 237 breq12d 
 |-  ( l = F -> ( ( ( C x.s l ) -s ( C x.s E ) )  ( ( C x.s F ) -s ( C x.s E ) )
239 233 238 imbi12d 
 |-  ( l = F -> ( ( ( C  ( ( C x.s l ) -s ( C x.s E ) )  ( ( C  ( ( C x.s F ) -s ( C x.s E ) )
240 239 anbi2d 
 |-  ( l = F -> ( ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s E ) )  ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s F ) -s ( C x.s E ) )
241 231 240 imbi12d 
 |-  ( l = F -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s l ) -s ( C x.s E ) )  ( x = ( ( ( 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 ) )
242 163 171 188 205 223 241 rspc6v 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i  ( ( i x.s l ) -s ( i x.s k ) )  ( x = ( ( ( 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 ) )
243 155 242 syl5com 
 |-  ( x e. On -> ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( x = ( ( ( 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 ) )
244 243 com23 
 |-  ( x e. On -> ( x = ( ( ( 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 e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s F ) -s ( C x.s E ) )
245 244 rexlimiv 
 |-  ( E. x e. On x = ( ( ( 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 e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s F ) -s ( C x.s E ) )
246 22 245 ax-mp 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C  ( ( C x.s F ) -s ( C x.s E ) )