Metamath Proof Explorer

Theorem mulsproplemcbv

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis 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 ) )
Assertion 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 ) )

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