Theorem addsproplem6

Description: Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when Y and Z are the same age. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsproplem.1	No typesetting found for |- ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
	addspropord.2	$$⊢\phi \to X\in \mathrm{No}$$
	addspropord.3	$$⊢\phi \to Y\in \mathrm{No}$$
	addspropord.4	$$⊢\phi \to Z\in \mathrm{No}$$
	addspropord.5	$$⊢\phi \to Y{<}_{s}Z$$
	addsproplem6.6	$$⊢\phi \to \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)$$
Assertion	addsproplem6	Could not format assertion : No typesetting found for |- ( ph -> ( Y +s X )

Proof

Step	Hyp	Ref	Expression
1		addsproplem.1	Could not format ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
2		addspropord.2	$$⊢\phi \to X\in \mathrm{No}$$
3		addspropord.3	$$⊢\phi \to Y\in \mathrm{No}$$
4		addspropord.4	$$⊢\phi \to Z\in \mathrm{No}$$
5		addspropord.5	$$⊢\phi \to Y{<}_{s}Z$$
6		addsproplem6.6	$$⊢\phi \to \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)$$
7		nodense	$$⊢\left(\left(Y\in \mathrm{No}\wedge Z\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\wedge Y{<}_{s}Z\right)\right)\to \exists m\in \mathrm{No}\left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)$$
8	3 4 6 5 7	syl22anc	$$⊢\phi \to \exists m\in \mathrm{No}\left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)$$
9	1 2 3	addsproplem3	Could not format ( ph -> ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) < ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
10	9	simp1d	Could not format ( ph -> ( X +s Y ) e. No ) : No typesetting found for |- ( ph -> ( X +s Y ) e. No ) with typecode |-
11	10	adantr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Y ) e. No ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Y ) e. No ) with typecode |-
12	1	adantr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
13	2	adantr	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to X\in \mathrm{No}$$
14		simprl	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to m\in \mathrm{No}$$
15		unidm	Could not format ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` m ) ) ) = ( ( bday ` X ) +no ( bday ` m ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` m ) ) ) = ( ( bday ` X ) +no ( bday ` m ) ) with typecode |-
16		simprr1	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)$$
17		bdayelon	$$⊢\mathrm{bday}\left(m\right)\in \mathrm{On}$$
18		bdayelon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}$$
19		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
20		naddel2	Could not format ( ( ( bday ` m ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` m ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
21	17 18 19 20	mp3an	Could not format ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
22	16 21	sylib	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
23		elun1	Could not format ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
24	22 23	syl	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
25	15 24	eqeltrid	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` m ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` m ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
26	12 13 14 14 25	addsproplem1	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( X +s m ) e. No /\ ( m ( m +s X ) ( ( X +s m ) e. No /\ ( m ( m +s X )
27	26	simpld	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. No ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. No ) with typecode |-
28		uncom	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
29	28	eleq2i	Could not format ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) <-> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) <-> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
30	29	imbi1i	Could not format ( ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
31	30	ralbii	Could not format ( A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( x +s y ) e. No /\ ( y ( y +s x ) A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
32	31	2ralbii	Could not format ( A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
33	1 32	sylib	Could not format ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
34	33 2 4	addsproplem3	Could not format ( ph -> ( ( X +s Z ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) < ( ( X +s Z ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) <
35	34	simp1d	Could not format ( ph -> ( X +s Z ) e. No ) : No typesetting found for |- ( ph -> ( X +s Z ) e. No ) with typecode |-
36	35	adantr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Z ) e. No ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Z ) e. No ) with typecode |-
37	9	simp3d	Could not format ( ph -> { ( X +s Y ) } < { ( X +s Y ) } <
38	37	adantr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y { ( X +s Y ) } < { ( X +s Y ) } <
39		ovex	Could not format ( X +s Y ) e. _V : No typesetting found for |- ( X +s Y ) e. _V with typecode |-
40	39	snid	Could not format ( X +s Y ) e. { ( X +s Y ) } : No typesetting found for |- ( X +s Y ) e. { ( X +s Y ) } with typecode |-
41	40	a1i	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Y ) e. { ( X +s Y ) } ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Y ) e. { ( X +s Y ) } ) with typecode |-
42		oldbday	$$⊢\left(\mathrm{bday}\left(Y\right)\in \mathrm{On}\wedge m\in \mathrm{No}\right)\to \left(m\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\leftrightarrow \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\right)$$
43	18 14 42	sylancr	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to \left(m\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\leftrightarrow \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\right)$$
44	16 43	mpbird	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to m\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)$$
45		simprr2	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to Y{<}_{s}m$$
46		breq2	$$⊢a=m\to \left(Y{<}_{s}a\leftrightarrow Y{<}_{s}m\right)$$
47		rightval	Could not format ( _Right ` Y ) = { a e. ( _Old ` ( bday ` Y ) ) | Y
48	46 47	elrab2	Could not format ( m e. ( _Right ` Y ) <-> ( m e. ( _Old ` ( bday ` Y ) ) /\ Y ( m e. ( _Old ` ( bday ` Y ) ) /\ Y
49	44 45 48	sylanbrc	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y m e. ( _Right ` Y ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y m e. ( _Right ` Y ) ) with typecode |-
50		eqid	Could not format ( X +s m ) = ( X +s m ) : No typesetting found for |- ( X +s m ) = ( X +s m ) with typecode |-
51		oveq2	Could not format ( h = m -> ( X +s h ) = ( X +s m ) ) : No typesetting found for |- ( h = m -> ( X +s h ) = ( X +s m ) ) with typecode |-
52	51	rspceeqv	Could not format ( ( m e. ( _Right ` Y ) /\ ( X +s m ) = ( X +s m ) ) -> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) : No typesetting found for |- ( ( m e. ( _Right ` Y ) /\ ( X +s m ) = ( X +s m ) ) -> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) with typecode |-
53	49 50 52	sylancl	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) with typecode |-
54		ovex	Could not format ( X +s m ) e. _V : No typesetting found for |- ( X +s m ) e. _V with typecode |-
55		eqeq1	Could not format ( g = ( X +s m ) -> ( g = ( X +s h ) <-> ( X +s m ) = ( X +s h ) ) ) : No typesetting found for |- ( g = ( X +s m ) -> ( g = ( X +s h ) <-> ( X +s m ) = ( X +s h ) ) ) with typecode |-
56	55	rexbidv	Could not format ( g = ( X +s m ) -> ( E. h e. ( _Right ` Y ) g = ( X +s h ) <-> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) ) : No typesetting found for |- ( g = ( X +s m ) -> ( E. h e. ( _Right ` Y ) g = ( X +s h ) <-> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) ) with typecode |-
57	54 56	elab	Could not format ( ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } <-> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) : No typesetting found for |- ( ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } <-> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) with typecode |-
58	53 57	sylibr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) with typecode |-
59		elun2	Could not format ( ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } -> ( X +s m ) e. ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) ) : No typesetting found for |- ( ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } -> ( X +s m ) e. ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) ) with typecode |-
60	58 59	syl	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) ) with typecode |-
61	38 41 60	ssltsepcd	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Y ) ( X +s Y )
62	33	adantr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
63	4	adantr	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to Z\in \mathrm{No}$$
64	62 13 63	addsproplem3	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( ( X +s Z ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) < ( ( X +s Z ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) <
65	64	simp2d	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) < ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) <
66	6	adantr	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)$$
67	16 66	eleqtrd	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Z\right)$$
68		bdayelon	$$⊢\mathrm{bday}\left(Z\right)\in \mathrm{On}$$
69		oldbday	$$⊢\left(\mathrm{bday}\left(Z\right)\in \mathrm{On}\wedge m\in \mathrm{No}\right)\to \left(m\in \mathrm{Old}\left(\mathrm{bday}\left(Z\right)\right)\leftrightarrow \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Z\right)\right)$$
70	68 14 69	sylancr	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to \left(m\in \mathrm{Old}\left(\mathrm{bday}\left(Z\right)\right)\leftrightarrow \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Z\right)\right)$$
71	67 70	mpbird	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to m\in \mathrm{Old}\left(\mathrm{bday}\left(Z\right)\right)$$
72		simprr3	$$⊢\left(\phi \wedge \left(m\in \mathrm{No}\wedge \left(\mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\wedge Y{<}_{s}m\wedge m{<}_{s}Z\right)\right)\right)\to m{<}_{s}Z$$
73		breq1	$$⊢a=m\to \left(a{<}_{s}Z\leftrightarrow m{<}_{s}Z\right)$$
74		leftval	Could not format ( _Left ` Z ) = { a e. ( _Old ` ( bday ` Z ) ) | a
75	73 74	elrab2	Could not format ( m e. ( _Left ` Z ) <-> ( m e. ( _Old ` ( bday ` Z ) ) /\ m ( m e. ( _Old ` ( bday ` Z ) ) /\ m
76	71 72 75	sylanbrc	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y m e. ( _Left ` Z ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y m e. ( _Left ` Z ) ) with typecode |-
77		oveq2	Could not format ( d = m -> ( X +s d ) = ( X +s m ) ) : No typesetting found for |- ( d = m -> ( X +s d ) = ( X +s m ) ) with typecode |-
78	77	rspceeqv	Could not format ( ( m e. ( _Left ` Z ) /\ ( X +s m ) = ( X +s m ) ) -> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) : No typesetting found for |- ( ( m e. ( _Left ` Z ) /\ ( X +s m ) = ( X +s m ) ) -> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) with typecode |-
79	76 50 78	sylancl	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) with typecode |-
80		eqeq1	Could not format ( c = ( X +s m ) -> ( c = ( X +s d ) <-> ( X +s m ) = ( X +s d ) ) ) : No typesetting found for |- ( c = ( X +s m ) -> ( c = ( X +s d ) <-> ( X +s m ) = ( X +s d ) ) ) with typecode |-
81	80	rexbidv	Could not format ( c = ( X +s m ) -> ( E. d e. ( _Left ` Z ) c = ( X +s d ) <-> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) ) : No typesetting found for |- ( c = ( X +s m ) -> ( E. d e. ( _Left ` Z ) c = ( X +s d ) <-> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) ) with typecode |-
82	54 81	elab	Could not format ( ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } <-> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) : No typesetting found for |- ( ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } <-> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) with typecode |-
83	79 82	sylibr	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) with typecode |-
84		elun2	Could not format ( ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } -> ( X +s m ) e. ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) ) : No typesetting found for |- ( ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } -> ( X +s m ) e. ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) ) with typecode |-
85	83 84	syl	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) e. ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) ) with typecode |-
86		ovex	Could not format ( X +s Z ) e. _V : No typesetting found for |- ( X +s Z ) e. _V with typecode |-
87	86	snid	Could not format ( X +s Z ) e. { ( X +s Z ) } : No typesetting found for |- ( X +s Z ) e. { ( X +s Z ) } with typecode |-
88	87	a1i	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Z ) e. { ( X +s Z ) } ) : No typesetting found for |- ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Z ) e. { ( X +s Z ) } ) with typecode |-
89	65 85 88	ssltsepcd	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s m ) ( X +s m )
90	11 27 36 61 89	slttrd	Could not format ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y ( X +s Y ) ( X +s Y )
91	8 90	rexlimddv	Could not format ( ph -> ( X +s Y ) ( X +s Y )
92	3 2	addscomd	Could not format ( ph -> ( Y +s X ) = ( X +s Y ) ) : No typesetting found for |- ( ph -> ( Y +s X ) = ( X +s Y ) ) with typecode |-
93	4 2	addscomd	Could not format ( ph -> ( Z +s X ) = ( X +s Z ) ) : No typesetting found for |- ( ph -> ( Z +s X ) = ( X +s Z ) ) with typecode |-
94	91 92 93	3brtr4d	Could not format ( ph -> ( Y +s X ) ( Y +s X )