Theorem mulsproplem13

Description: Lemma for surreal multiplication. Remove the restriction on C and D from mulsproplem12 . (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
	mulsproplem13.1	|- ( ph -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
Assertion	mulsproplem13	|- ( 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		mulsproplem13.1	|- ( ph -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
9	1	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> 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 ) )
10	2	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> C e. No )
11	3	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> D e. No )
12	4	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> E e. No )
13	5	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> F e. No )
14	6	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> C
15	7	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> E
16		simpr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) )
17	8	adantr	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
18	9 10 11 12 13 14 15 16 17	mulsproplem12	|- ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
19	2	adantr	|- ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> C e. No )
20	3	adantr	|- ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> D e. No )
21		simpr	|- ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> ( bday ` C ) = ( bday ` D ) )
22	6	adantr	|- ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> C
23		nodense	|- ( ( ( C e. No /\ D e. No ) /\ ( ( bday ` C ) = ( bday ` D ) /\ C E. x e. No ( ( bday ` x ) e. ( bday ` C ) /\ C
24	19 20 21 22 23	syl22anc	|- ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> E. x e. No ( ( bday ` x ) e. ( bday ` C ) /\ C
25		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 ) ) )
26		unidm	|- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) )
27		bday0s	|- ( bday ` 0s ) = (/)
28	27 27	oveq12i	|- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) )
29		0elon	|- (/) e. On
30		naddrid	|- ( (/) e. On -> ( (/) +no (/) ) = (/) )
31	29 30	ax-mp	|- ( (/) +no (/) ) = (/)
32	28 31	eqtri	|- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/)
33	25 26 32	3eqtri	|- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/)
34	33	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. (/) )
35		un0	|- ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) )
36	34 35	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 ) )
37		ssun1	|- ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
38		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 ) ) ) )
39	37 38	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 ) ) ) )
40		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 ) ) ) ) )
41	39 40	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 ) ) ) ) )
42	36 41	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 ) ) ) ) )
43	42	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 ) ) ) ) ) )
44	43	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 ) )
45	44	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 ) )
46	1 45	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 ) )
47	46 2 5	mulsproplem11	|- ( ph -> ( C x.s F ) e. No )
48	33	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. (/) )
49		un0	|- ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) )
50	48 49	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 ) )
51		ssun1	|- ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
52		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 ) ) ) )
53	51 52	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 ) ) ) )
54	53 40	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 ) ) ) ) )
55	50 54	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 ) ) ) ) )
56	55	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 ) ) ) ) ) )
57	56	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 ) )
58	57	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 ) )
59	1 58	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 ) )
60	59 2 4	mulsproplem11	|- ( ph -> ( C x.s E ) e. No )
61	47 60	subscld	|- ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No )
62	61	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) ) e. No )
63	46	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ) )
64		simprr1	|- ( ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( bday ` x ) e. ( bday ` C ) )
65	64	adantl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( bday ` x ) e. ( bday ` C ) )
66		bdayelon	|- ( bday ` C ) e. On
67		simprrl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C x e. No )
68		oldbday	|- ( ( ( bday ` C ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` C ) ) <-> ( bday ` x ) e. ( bday ` C ) ) )
69	66 67 68	sylancr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x e. ( _Old ` ( bday ` C ) ) <-> ( bday ` x ) e. ( bday ` C ) ) )
70	65 69	mpbird	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C x e. ( _Old ` ( bday ` C ) ) )
71	5	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C F e. No )
72	63 70 71	mulsproplem2	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x x.s F ) e. No )
73	59	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ) )
74	4	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C E e. No )
75	73 70 74	mulsproplem2	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x x.s E ) e. No )
76	72 75	subscld	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( x x.s F ) -s ( x x.s E ) ) e. No )
77	33	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. (/) )
78		un0	|- ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) )
79	77 78	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 ) )
80		ssun2	|- ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) )
81	80 52	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 ) ) ) )
82	81 40	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 ) ) ) ) )
83	79 82	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 ) ) ) ) )
84	83	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 ) ) ) ) ) )
85	84	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 ) )
86	85	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 ) )
87	1 86	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 ) )
88	87 3 5	mulsproplem11	|- ( ph -> ( D x.s F ) e. No )
89	33	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. (/) )
90		un0	|- ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) )
91	89 90	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 ) )
92		ssun2	|- ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) )
93	92 38	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 ) ) ) )
94	93 40	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 ) ) ) ) )
95	91 94	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 ) ) ) ) )
96	95	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 ) ) ) ) ) )
97	96	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 ) )
98	97	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 ) )
99	1 98	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 ) )
100	99 3 4	mulsproplem11	|- ( ph -> ( D x.s E ) e. No )
101	88 100	subscld	|- ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No )
102	101	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( D x.s F ) -s ( D x.s E ) ) e. No )
103	1	mulsproplemcbv	|- ( ph -> A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
104	103	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
105		onelss	|- ( ( bday ` C ) e. On -> ( ( bday ` x ) e. ( bday ` C ) -> ( bday ` x ) C_ ( bday ` C ) ) )
106	66 65 105	mpsyl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( bday ` x ) C_ ( bday ` C ) )
107		simprl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( bday ` C ) = ( bday ` D ) )
108	106 107	sseqtrd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( bday ` x ) C_ ( bday ` D ) )
109		bdayelon	|- ( bday ` x ) e. On
110		bdayelon	|- ( bday ` D ) e. On
111		bdayelon	|- ( bday ` F ) e. On
112		naddss1	|- ( ( ( bday ` x ) e. On /\ ( bday ` D ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) )
113	109 110 111 112	mp3an	|- ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) )
114	108 113	sylib	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) )
115		unss2	|- ( ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) )
116	114 115	syl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) )
117		bdayelon	|- ( bday ` E ) e. On
118		naddss1	|- ( ( ( bday ` x ) e. On /\ ( bday ` D ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) )
119	109 110 117 118	mp3an	|- ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) )
120	108 119	sylib	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) )
121		unss2	|- ( ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
122	120 121	syl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
123		unss12	|- ( ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ) ) ) ) )
124	116 122 123	syl2anc	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ) ) ) ) )
125		unss2	|- ( ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ) ) ) ) ) )
126	124 125	syl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ) ) ) ) ) )
127	126	sseld	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( 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. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` 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. ( ( ( 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 ) ) ) ) ) ) )
128	127	imim1d	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s 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 ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
129	128	ralimd6v	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
130	104 129	mpd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
131	2	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C C e. No )
132		simprr2	|- ( ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C C
133	132	adantl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C C
134	7	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C E
135	65	olcd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` C ) e. ( bday ` x ) \/ ( bday ` x ) e. ( bday ` C ) ) )
136	8	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` E ) e. ( bday ` F ) \/ ( bday ` F ) e. ( bday ` E ) ) )
137	130 131 67 74 71 133 134 135 136	mulsproplem12	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) )
138		naddss1	|- ( ( ( bday ` x ) e. On /\ ( bday ` C ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) )
139	109 66 117 138	mp3an	|- ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) )
140	106 139	sylib	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) )
141		unss1	|- ( ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) -> ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) )
142	140 141	syl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) )
143		naddss1	|- ( ( ( bday ` x ) e. On /\ ( bday ` C ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) )
144	109 66 111 143	mp3an	|- ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) )
145	106 144	sylib	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) )
146		unss1	|- ( ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) -> ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
147	145 146	syl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) )
148		unss12	|- ( ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) ) ) ) )
149	142 147 148	syl2anc	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) ) ) ) )
150		unss2	|- ( ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) ) ) ) ) )
151	149 150	syl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) ) ) ) ) )
152	151	sseld	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( 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. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` 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. ( ( ( 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 ) ) ) ) ) ) )
153	152	imim1d	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s 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 ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
154	153	ralimd6v	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
155	104 154	mpd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
156	3	adantr	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C D e. No )
157		simprr3	|- ( ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C x
158	157	adantl	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C x
159	65 107	eleqtrd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( bday ` x ) e. ( bday ` D ) )
160	159	orcd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` x ) ) )
161	155 67 156 74 71 158 134 160 136	mulsproplem12	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( x x.s F ) -s ( x x.s E ) )
162	62 76 102 137 161	slttrd	|- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) )
163	162	anassrs	|- ( ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) )
164	24 163	rexlimddv	|- ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> ( ( C x.s F ) -s ( C x.s E ) )
165	66	onordi	|- Ord ( bday ` C )
166	110	onordi	|- Ord ( bday ` D )
167		ordtri3or	|- ( ( Ord ( bday ` C ) /\ Ord ( bday ` D ) ) -> ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` C ) = ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) )
168	165 166 167	mp2an	|- ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` C ) = ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) )
169		df-3or	|- ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` C ) = ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) <-> ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` C ) = ( bday ` D ) ) \/ ( bday ` D ) e. ( bday ` C ) ) )
170		or32	|- ( ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` C ) = ( bday ` D ) ) \/ ( bday ` D ) e. ( bday ` C ) ) <-> ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) \/ ( bday ` C ) = ( bday ` D ) ) )
171	169 170	bitri	|- ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` C ) = ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) <-> ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) \/ ( bday ` C ) = ( bday ` D ) ) )
172	168 171	mpbi	|- ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) \/ ( bday ` C ) = ( bday ` D ) )
173	172	a1i	|- ( ph -> ( ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) \/ ( bday ` C ) = ( bday ` D ) ) )
174	18 164 173	mpjaodan	|- ( ph -> ( ( C x.s F ) -s ( C x.s E ) )