Theorem mulsproplem1

Description: Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	No typesetting found for |- ( 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	$$⊢\phi \to X\in \mathrm{No}$$
	mulsproplem1.2	$$⊢\phi \to Y\in \mathrm{No}$$
	mulsproplem1.3	$$⊢\phi \to Z\in \mathrm{No}$$
	mulsproplem1.4	$$⊢\phi \to W\in \mathrm{No}$$
	mulsproplem1.5	$$⊢\phi \to T\in \mathrm{No}$$
	mulsproplem1.6	$$⊢\phi \to U\in \mathrm{No}$$
	mulsproplem1.7	No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
Assertion	mulsproplem1	Could not format assertion : No typesetting found for |- ( 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	Could not format ( 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 ) ) 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	$$⊢\phi \to X\in \mathrm{No}$$
3		mulsproplem1.2	$$⊢\phi \to Y\in \mathrm{No}$$
4		mulsproplem1.3	$$⊢\phi \to Z\in \mathrm{No}$$
5		mulsproplem1.4	$$⊢\phi \to W\in \mathrm{No}$$
6		mulsproplem1.5	$$⊢\phi \to T\in \mathrm{No}$$
7		mulsproplem1.6	$$⊢\phi \to U\in \mathrm{No}$$
8		mulsproplem1.7	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
9		fveq2	$$⊢a=X\to \mathrm{bday}\left(a\right)=\mathrm{bday}\left(X\right)$$
10	9	oveq1d	Could not format ( a = X -> ( ( bday ` a ) +no ( bday ` b ) ) = ( ( bday ` X ) +no ( bday ` b ) ) ) : No typesetting found for |- ( a = X -> ( ( bday ` a ) +no ( bday ` b ) ) = ( ( bday ` X ) +no ( bday ` b ) ) ) with typecode |-
11	10	uneq1d	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
12	11	eleq1d	Could not format ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) with typecode |-
13		oveq1	Could not format ( a = X -> ( a x.s b ) = ( X x.s b ) ) : No typesetting found for |- ( a = X -> ( a x.s b ) = ( X x.s b ) ) with typecode |-
14	13	eleq1d	Could not format ( a = X -> ( ( a x.s b ) e. No <-> ( X x.s b ) e. No ) ) : No typesetting found for |- ( a = X -> ( ( a x.s b ) e. No <-> ( X x.s b ) e. No ) ) with typecode |-
15	14	anbi1d	Could not format ( 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 ) ) ( ( ( 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	Could not format ( 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 ) ) ( ( ( ( ( bday ` a ) +no ( bday ` b ) ) 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\to \mathrm{bday}\left(b\right)=\mathrm{bday}\left(Y\right)$$
18	17	oveq2d	Could not format ( b = Y -> ( ( bday ` X ) +no ( bday ` b ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( b = Y -> ( ( bday ` X ) +no ( bday ` b ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
19	18	uneq1d	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
20	19	eleq1d	Could not format ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) with typecode |-
21		oveq2	Could not format ( b = Y -> ( X x.s b ) = ( X x.s Y ) ) : No typesetting found for |- ( b = Y -> ( X x.s b ) = ( X x.s Y ) ) with typecode |-
22	21	eleq1d	Could not format ( b = Y -> ( ( X x.s b ) e. No <-> ( X x.s Y ) e. No ) ) : No typesetting found for |- ( b = Y -> ( ( X x.s b ) e. No <-> ( X x.s Y ) e. No ) ) with typecode |-
23	22	anbi1d	Could not format ( 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 ) ) ( ( ( 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	Could not format ( 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 ) ) ( ( ( ( ( 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\to \mathrm{bday}\left(c\right)=\mathrm{bday}\left(Z\right)$$
26	25	oveq1d	Could not format ( c = Z -> ( ( bday ` c ) +no ( bday ` e ) ) = ( ( bday ` Z ) +no ( bday ` e ) ) ) : No typesetting found for |- ( c = Z -> ( ( bday ` c ) +no ( bday ` e ) ) = ( ( bday ` Z ) +no ( bday ` e ) ) ) with typecode |-
27	26	uneq1d	Could not format ( c = Z -> ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) ) : No typesetting found for |- ( c = Z -> ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) ) with typecode |-
28	25	oveq1d	Could not format ( c = Z -> ( ( bday ` c ) +no ( bday ` f ) ) = ( ( bday ` Z ) +no ( bday ` f ) ) ) : No typesetting found for |- ( c = Z -> ( ( bday ` c ) +no ( bday ` f ) ) = ( ( bday ` Z ) +no ( bday ` f ) ) ) with typecode |-
29	28	uneq1d	Could not format ( c = Z -> ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) : No typesetting found for |- ( c = Z -> ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) with typecode |-
30	27 29	uneq12d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
31	30	uneq2d	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
32	31	eleq1d	Could not format ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) with typecode |-
33		breq1	$$⊢c=Z\to \left(c{<}_{s}d\leftrightarrow Z{<}_{s}d\right)$$
34	33	anbi1d	$$⊢c=Z\to \left(\left(c{<}_{s}d\wedge e{<}_{s}f\right)\leftrightarrow \left(Z{<}_{s}d\wedge e{<}_{s}f\right)\right)$$
35		oveq1	Could not format ( c = Z -> ( c x.s f ) = ( Z x.s f ) ) : No typesetting found for |- ( c = Z -> ( c x.s f ) = ( Z x.s f ) ) with typecode |-
36		oveq1	Could not format ( c = Z -> ( c x.s e ) = ( Z x.s e ) ) : No typesetting found for |- ( c = Z -> ( c x.s e ) = ( Z x.s e ) ) with typecode |-
37	35 36	oveq12d	Could not format ( c = Z -> ( ( c x.s f ) -s ( c x.s e ) ) = ( ( Z x.s f ) -s ( Z x.s e ) ) ) : No typesetting found for |- ( c = Z -> ( ( c x.s f ) -s ( c x.s e ) ) = ( ( Z x.s f ) -s ( Z x.s e ) ) ) with typecode |-
38	37	breq1d	Could not format ( c = Z -> ( ( ( c x.s f ) -s ( c x.s e ) ) ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( ( c x.s f ) -s ( c x.s e ) ) ( ( Z x.s f ) -s ( Z x.s e ) )
39	34 38	imbi12d	Could not format ( c = Z -> ( ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
40	39	anbi2d	Could not format ( 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 ) ) ( ( ( 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	Could not format ( 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 ) ) ( ( ( ( ( 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\to \mathrm{bday}\left(d\right)=\mathrm{bday}\left(W\right)$$
43	42	oveq1d	Could not format ( d = W -> ( ( bday ` d ) +no ( bday ` f ) ) = ( ( bday ` W ) +no ( bday ` f ) ) ) : No typesetting found for |- ( d = W -> ( ( bday ` d ) +no ( bday ` f ) ) = ( ( bday ` W ) +no ( bday ` f ) ) ) with typecode |-
44	43	uneq2d	Could not format ( d = W -> ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) ) : No typesetting found for |- ( d = W -> ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) ) with typecode |-
45	42	oveq1d	Could not format ( d = W -> ( ( bday ` d ) +no ( bday ` e ) ) = ( ( bday ` W ) +no ( bday ` e ) ) ) : No typesetting found for |- ( d = W -> ( ( bday ` d ) +no ( bday ` e ) ) = ( ( bday ` W ) +no ( bday ` e ) ) ) with typecode |-
46	45	uneq2d	Could not format ( d = W -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) ) : No typesetting found for |- ( d = W -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) ) with typecode |-
47	44 46	uneq12d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
48	47	uneq2d	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
49	48	eleq1d	Could not format ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) with typecode |-
50		breq2	$$⊢d=W\to \left(Z{<}_{s}d\leftrightarrow Z{<}_{s}W\right)$$
51	50	anbi1d	$$⊢d=W\to \left(\left(Z{<}_{s}d\wedge e{<}_{s}f\right)\leftrightarrow \left(Z{<}_{s}W\wedge e{<}_{s}f\right)\right)$$
52		oveq1	Could not format ( d = W -> ( d x.s f ) = ( W x.s f ) ) : No typesetting found for |- ( d = W -> ( d x.s f ) = ( W x.s f ) ) with typecode |-
53		oveq1	Could not format ( d = W -> ( d x.s e ) = ( W x.s e ) ) : No typesetting found for |- ( d = W -> ( d x.s e ) = ( W x.s e ) ) with typecode |-
54	52 53	oveq12d	Could not format ( d = W -> ( ( d x.s f ) -s ( d x.s e ) ) = ( ( W x.s f ) -s ( W x.s e ) ) ) : No typesetting found for |- ( d = W -> ( ( d x.s f ) -s ( d x.s e ) ) = ( ( W x.s f ) -s ( W x.s e ) ) ) with typecode |-
55	54	breq2d	Could not format ( d = W -> ( ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z x.s f ) -s ( Z x.s e ) )
56	51 55	imbi12d	Could not format ( d = W -> ( ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) )
57	56	anbi2d	Could not format ( 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 ) ) ( ( ( 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	Could not format ( 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 ) ) ( ( ( ( ( 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\to \mathrm{bday}\left(e\right)=\mathrm{bday}\left(T\right)$$
60	59	oveq2d	Could not format ( e = T -> ( ( bday ` Z ) +no ( bday ` e ) ) = ( ( bday ` Z ) +no ( bday ` T ) ) ) : No typesetting found for |- ( e = T -> ( ( bday ` Z ) +no ( bday ` e ) ) = ( ( bday ` Z ) +no ( bday ` T ) ) ) with typecode |-
61	60	uneq1d	Could not format ( e = T -> ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) ) : No typesetting found for |- ( e = T -> ( ( ( bday ` Z ) +no ( bday ` e ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) ) with typecode |-
62	59	oveq2d	Could not format ( e = T -> ( ( bday ` W ) +no ( bday ` e ) ) = ( ( bday ` W ) +no ( bday ` T ) ) ) : No typesetting found for |- ( e = T -> ( ( bday ` W ) +no ( bday ` e ) ) = ( ( bday ` W ) +no ( bday ` T ) ) ) with typecode |-
63	62	uneq2d	Could not format ( e = T -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) : No typesetting found for |- ( e = T -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` e ) ) ) = ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) with typecode |-
64	61 63	uneq12d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
65	64	uneq2d	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
66	65	eleq1d	Could not format ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) with typecode |-
67		breq1	$$⊢e=T\to \left(e{<}_{s}f\leftrightarrow T{<}_{s}f\right)$$
68	67	anbi2d	$$⊢e=T\to \left(\left(Z{<}_{s}W\wedge e{<}_{s}f\right)\leftrightarrow \left(Z{<}_{s}W\wedge T{<}_{s}f\right)\right)$$
69		oveq2	Could not format ( e = T -> ( Z x.s e ) = ( Z x.s T ) ) : No typesetting found for |- ( e = T -> ( Z x.s e ) = ( Z x.s T ) ) with typecode |-
70	69	oveq2d	Could not format ( e = T -> ( ( Z x.s f ) -s ( Z x.s e ) ) = ( ( Z x.s f ) -s ( Z x.s T ) ) ) : No typesetting found for |- ( e = T -> ( ( Z x.s f ) -s ( Z x.s e ) ) = ( ( Z x.s f ) -s ( Z x.s T ) ) ) with typecode |-
71		oveq2	Could not format ( e = T -> ( W x.s e ) = ( W x.s T ) ) : No typesetting found for |- ( e = T -> ( W x.s e ) = ( W x.s T ) ) with typecode |-
72	71	oveq2d	Could not format ( e = T -> ( ( W x.s f ) -s ( W x.s e ) ) = ( ( W x.s f ) -s ( W x.s T ) ) ) : No typesetting found for |- ( e = T -> ( ( W x.s f ) -s ( W x.s e ) ) = ( ( W x.s f ) -s ( W x.s T ) ) ) with typecode |-
73	70 72	breq12d	Could not format ( e = T -> ( ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z x.s f ) -s ( Z x.s T ) )
74	68 73	imbi12d	Could not format ( e = T -> ( ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( ( Z ( ( Z x.s f ) -s ( Z x.s e ) ) ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) )
75	74	anbi2d	Could not format ( 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 ) ) ( ( ( 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	Could not format ( 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 ) ) ( ( ( ( ( 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\to \mathrm{bday}\left(f\right)=\mathrm{bday}\left(U\right)$$
78	77	oveq2d	Could not format ( f = U -> ( ( bday ` W ) +no ( bday ` f ) ) = ( ( bday ` W ) +no ( bday ` U ) ) ) : No typesetting found for |- ( f = U -> ( ( bday ` W ) +no ( bday ` f ) ) = ( ( bday ` W ) +no ( bday ` U ) ) ) with typecode |-
79	78	uneq2d	Could not format ( f = U -> ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) ) : No typesetting found for |- ( f = U -> ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` f ) ) ) = ( ( ( bday ` Z ) +no ( bday ` T ) ) u. ( ( bday ` W ) +no ( bday ` U ) ) ) ) with typecode |-
80	77	oveq2d	Could not format ( f = U -> ( ( bday ` Z ) +no ( bday ` f ) ) = ( ( bday ` Z ) +no ( bday ` U ) ) ) : No typesetting found for |- ( f = U -> ( ( bday ` Z ) +no ( bday ` f ) ) = ( ( bday ` Z ) +no ( bday ` U ) ) ) with typecode |-
81	80	uneq1d	Could not format ( f = U -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) = ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) : No typesetting found for |- ( f = U -> ( ( ( bday ` Z ) +no ( bday ` f ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) = ( ( ( bday ` Z ) +no ( bday ` U ) ) u. ( ( bday ` W ) +no ( bday ` T ) ) ) ) with typecode |-
82	79 81	uneq12d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
83	82	uneq2d	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) with typecode |-
84	83	eleq1d	Could not format ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) with typecode |-
85		breq2	$$⊢f=U\to \left(T{<}_{s}f\leftrightarrow T{<}_{s}U\right)$$
86	85	anbi2d	$$⊢f=U\to \left(\left(Z{<}_{s}W\wedge T{<}_{s}f\right)\leftrightarrow \left(Z{<}_{s}W\wedge T{<}_{s}U\right)\right)$$
87		oveq2	Could not format ( f = U -> ( Z x.s f ) = ( Z x.s U ) ) : No typesetting found for |- ( f = U -> ( Z x.s f ) = ( Z x.s U ) ) with typecode |-
88	87	oveq1d	Could not format ( f = U -> ( ( Z x.s f ) -s ( Z x.s T ) ) = ( ( Z x.s U ) -s ( Z x.s T ) ) ) : No typesetting found for |- ( f = U -> ( ( Z x.s f ) -s ( Z x.s T ) ) = ( ( Z x.s U ) -s ( Z x.s T ) ) ) with typecode |-
89		oveq2	Could not format ( f = U -> ( W x.s f ) = ( W x.s U ) ) : No typesetting found for |- ( f = U -> ( W x.s f ) = ( W x.s U ) ) with typecode |-
90	89	oveq1d	Could not format ( f = U -> ( ( W x.s f ) -s ( W x.s T ) ) = ( ( W x.s U ) -s ( W x.s T ) ) ) : No typesetting found for |- ( f = U -> ( ( W x.s f ) -s ( W x.s T ) ) = ( ( W x.s U ) -s ( W x.s T ) ) ) with typecode |-
91	88 90	breq12d	Could not format ( f = U -> ( ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( Z x.s U ) -s ( Z x.s T ) ) ( ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( Z x.s U ) -s ( Z x.s T ) )
92	86 91	imbi12d	Could not format ( f = U -> ( ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) ) ( ( ( Z ( ( Z x.s f ) -s ( Z x.s T ) ) ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )
93	92	anbi2d	Could not format ( 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 ) ) ( ( ( 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	Could not format ( 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 ) ) ( ( ( ( ( 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	Could not format ( ( ( 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 ) ) ( 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	Could not format ( 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 ) ) ( 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	Could not format ( ph -> ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) ) ( ( X x.s Y ) e. No /\ ( ( Z ( ( Z x.s U ) -s ( Z x.s T ) )