Theorem mulsproplem1

Description: Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-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 ) )
	mulsproplem1.1	|- ( ph -> X e. No )
	mulsproplem1.2	|- ( ph -> Y e. No )
	mulsproplem1.3	|- ( ph -> Z e. No )
	mulsproplem1.4	|- ( ph -> W e. No )
	mulsproplem1.5	|- ( ph -> T e. No )
	mulsproplem1.6	|- ( ph -> U e. No )
	mulsproplem1.7	|- ( ph -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) )
Assertion	mulsproplem1	|- ( ph -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )

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		mulsproplem1.1	|- ( ph -> X e. No )
3		mulsproplem1.2	|- ( ph -> Y e. No )
4		mulsproplem1.3	|- ( ph -> Z e. No )
5		mulsproplem1.4	|- ( ph -> W e. No )
6		mulsproplem1.5	|- ( ph -> T e. No )
7		mulsproplem1.6	|- ( ph -> U e. No )
8		mulsproplem1.7	|- ( ph -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) )
9		fveq2	|- ( a = X -> ( bday ` a ) = ( bday ` X ) )
10	9	oveq1d	|- ( a = X -> ( ( bday ` a ) +no ( bday ` b ) ) = ( ( bday ` X ) +no ( bday ` b ) ) )
11	10	uneq1d	|- ( a = 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 ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) )
12	11	eleq1d	|- ( a = 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( bday ` X ) +no ( bday ` b ) ) 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 ) ) ) ) ) ) )
13		oveq1	|- ( a = X -> ( a x.s b ) = ( X x.s b ) )
14	13	eleq1d	|- ( a = X -> ( ( a x.s b ) e. No <-> ( X x.s b ) e. No ) )
15	14	anbi1d	|- ( a = X -> ( ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( X x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
16	12 15	imbi12d	|- ( a = 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 ) ) ) ) ) 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 ` X ) +no ( bday ` b ) ) 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 ) ) ) ) ) -> ( ( X x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
17		fveq2	|- ( b = Y -> ( bday ` b ) = ( bday ` Y ) )
18	17	oveq2d	|- ( b = Y -> ( ( bday ` X ) +no ( bday ` b ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) )
19	18	uneq1d	|- ( b = Y -> ( ( ( bday ` X ) +no ( bday ` b ) ) 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 ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) )
20	19	eleq1d	|- ( b = Y -> ( ( ( ( bday ` X ) +no ( bday ` b ) ) 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 ) ) ) ) ) <-> ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ) ) ) ) ) ) )
21		oveq2	|- ( b = Y -> ( X x.s b ) = ( X x.s Y ) )
22	21	eleq1d	|- ( b = Y -> ( ( X x.s b ) e. No <-> ( X x.s Y ) e. No ) )
23	22	anbi1d	|- ( b = Y -> ( ( ( X x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( X x.s Y ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
24	20 23	imbi12d	|- ( b = Y -> ( ( ( ( ( bday ` X ) +no ( bday ` b ) ) 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 ) ) ) ) ) -> ( ( X x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
25		fveq2	|- ( c = Z -> ( bday ` c ) = ( bday ` Z ) )
26	25	oveq1d	|- ( c = Z -> ( ( bday ` c ) +no ( bday ` e ) ) = ( ( bday ` Z ) +no ( bday ` e ) ) )
27	26	uneq1d	|- ( c = Z -> ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) )
28	25	oveq1d	|- ( c = Z -> ( ( bday ` c ) +no ( bday ` f ) ) = ( ( bday ` Z ) +no ( bday ` f ) ) )
29	28	uneq1d	|- ( c = Z -> ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) )
30	27 29	uneq12d	|- ( c = Z -> ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) )
31	30	uneq2d	|- ( c = Z -> ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) )
32	31	eleq1d	|- ( c = Z -> ( ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ) ) ) ) ) <-> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +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 ) ) ) ) ) ) )
33		breq1	|- ( c = Z -> ( c Z
34	33	anbi1d	|- ( c = Z -> ( ( c ( Z
35		oveq1	|- ( c = Z -> ( c x.s f ) = ( Z x.s f ) )
36		oveq1	|- ( c = Z -> ( c x.s e ) = ( Z x.s e ) )
37	35 36	oveq12d	|- ( c = Z -> ( ( c x.s f ) -s ( c x.s e ) ) = ( ( Z x.s f ) -s ( Z x.s e ) ) )
38	37	breq1d	|- ( c = Z -> ( ( ( c x.s f ) -s ( c x.s e ) ) ( ( Z x.s f ) -s ( Z x.s e ) )
39	34 38	imbi12d	|- ( c = Z -> ( ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
40	39	anbi2d	|- ( c = Z -> ( ( ( X x.s Y ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
41	32 40	imbi12d	|- ( c = Z -> ( ( ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
42		fveq2	|- ( d = W -> ( bday ` d ) = ( bday ` W ) )
43	42	oveq1d	|- ( d = W -> ( ( bday ` d ) +no ( bday ` f ) ) = ( ( bday ` W ) +no ( bday ` f ) ) )
44	43	uneq2d	|- ( d = W -> ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) )
45	42	oveq1d	|- ( d = W -> ( ( bday ` d ) +no ( bday ` e ) ) = ( ( bday ` W ) +no ( bday ` e ) ) )
46	45	uneq2d	|- ( d = W -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) )
47	44 46	uneq12d	|- ( d = W -> ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) ) )
48	47	uneq2d	|- ( d = W -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) ) ) )
49	48	eleq1d	|- ( d = W -> ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +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 ) ) ) ) ) <-> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +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 ) ) ) ) ) ) )
50		breq2	|- ( d = W -> ( Z Z
51	50	anbi1d	|- ( d = W -> ( ( Z ( Z
52		oveq1	|- ( d = W -> ( d x.s f ) = ( W x.s f ) )
53		oveq1	|- ( d = W -> ( d x.s e ) = ( W x.s e ) )
54	52 53	oveq12d	|- ( d = W -> ( ( d x.s f ) -s ( d x.s e ) ) = ( ( W x.s f ) -s ( W x.s e ) ) )
55	54	breq2d	|- ( d = W -> ( ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z x.s f ) -s ( Z x.s e ) )
56	51 55	imbi12d	|- ( d = W -> ( ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
57	56	anbi2d	|- ( d = W -> ( ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
58	49 57	imbi12d	|- ( d = W -> ( ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
59		fveq2	|- ( e = T -> ( bday ` e ) = ( bday ` T ) )
60	59	oveq2d	|- ( e = T -> ( ( bday ` Z ) +no ( bday ` e ) ) = ( ( bday ` Z ) +no ( bday ` T ) ) )
61	60	uneq1d	|- ( e = T -> ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) )
62	59	oveq2d	|- ( e = T -> ( ( bday ` W ) +no ( bday ` e ) ) = ( ( bday ` W ) +no ( bday ` T ) ) )
63	62	uneq2d	|- ( e = T -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) )
64	61 63	uneq12d	|- ( e = T -> ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) )
65	64	uneq2d	|- ( e = T -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) )
66	65	eleq1d	|- ( e = T -> ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +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 ) ) ) ) ) <-> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) ) )
67		breq1	|- ( e = T -> ( e T
68	67	anbi2d	|- ( e = T -> ( ( Z ( Z
69		oveq2	|- ( e = T -> ( Z x.s e ) = ( Z x.s T ) )
70	69	oveq2d	|- ( e = T -> ( ( Z x.s f ) -s ( Z x.s e ) ) = ( ( Z x.s f ) -s ( Z x.s T ) ) )
71		oveq2	|- ( e = T -> ( W x.s e ) = ( W x.s T ) )
72	71	oveq2d	|- ( e = T -> ( ( W x.s f ) -s ( W x.s e ) ) = ( ( W x.s f ) -s ( W x.s T ) ) )
73	70 72	breq12d	|- ( e = T -> ( ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z x.s f ) -s ( Z x.s T ) )
74	68 73	imbi12d	|- ( e = T -> ( ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) )
75	74	anbi2d	|- ( e = T -> ( ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) )
76	66 75	imbi12d	|- ( e = T -> ( ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) )
77		fveq2	|- ( f = U -> ( bday ` f ) = ( bday ` U ) )
78	77	oveq2d	|- ( f = U -> ( ( bday ` W ) +no ( bday ` f ) ) = ( ( bday ` W ) +no ( bday ` U ) ) )
79	78	uneq2d	|- ( f = U -> ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) )
80	77	oveq2d	|- ( f = U -> ( ( bday ` Z ) +no ( bday ` f ) ) = ( ( bday ` Z ) +no ( bday ` U ) ) )
81	80	uneq1d	|- ( f = U -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) = ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) )
82	79 81	uneq12d	|- ( f = U -> ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) = ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) )
83	82	uneq2d	|- ( f = U -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) )
84	83	eleq1d	|- ( f = U -> ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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		breq2	|- ( f = U -> ( T T
86	85	anbi2d	|- ( f = U -> ( ( Z ( Z
87		oveq2	|- ( f = U -> ( Z x.s f ) = ( Z x.s U ) )
88	87	oveq1d	|- ( f = U -> ( ( Z x.s f ) -s ( Z x.s T ) ) = ( ( Z x.s U ) -s ( Z x.s T ) ) )
89		oveq2	|- ( f = U -> ( W x.s f ) = ( W x.s U ) )
90	89	oveq1d	|- ( f = U -> ( ( W x.s f ) -s ( W x.s T ) ) = ( ( W x.s U ) -s ( W x.s T ) ) )
91	88 90	breq12d	|- ( f = U -> ( ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( Z x.s U ) -s ( Z x.s T ) )
92	86 91	imbi12d	|- ( f = U -> ( ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )
93	92	anbi2d	|- ( f = U -> ( ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )
94	84 93	imbi12d	|- ( f = U -> ( ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )
95	16 24 41 58 76 94	rspc6v	|- ( ( ( X e. No /\ Y e. No ) /\ ( Z e. No /\ W e. No ) /\ ( T e. No /\ U e. No ) ) -> ( 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 ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )
96	2 3 4 5 6 7 95	syl222anc	|- ( 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 ) ) ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) u. ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) ) 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 ) ) ) ) ) -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )
97	1 8 96	mp2d	|- ( ph -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )