Theorem addsproplem4

Description: Lemma for surreal addition properties. Show the second half of the inductive hypothesis when Y is older than Z . (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$$
	addsproplem4.6	$$⊢\phi \to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)$$
Assertion	addsproplem4	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		addsproplem4.6	$$⊢\phi \to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)$$
7		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 |-
8	7	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 |-
9	8	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 )
10	9	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 )
11	10	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 )
12	1 11	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 )
13	12 2 4	addsproplem3	Could not format ( ph -> ( ( X +s Z ) e. No /\ ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) < ( ( X +s Z ) e. No /\ ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) <
14	13	simp2d	Could not format ( ph -> ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) < ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) <
15		bdayelon	$$⊢\mathrm{bday}\left(Z\right)\in \mathrm{On}$$
16		oldbday	$$⊢\left(\mathrm{bday}\left(Z\right)\in \mathrm{On}\wedge Y\in \mathrm{No}\right)\to \left(Y\in \mathrm{Old}\left(\mathrm{bday}\left(Z\right)\right)\leftrightarrow \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)$$
17	15 3 16	sylancr	$$⊢\phi \to \left(Y\in \mathrm{Old}\left(\mathrm{bday}\left(Z\right)\right)\leftrightarrow \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)$$
18	6 17	mpbird	$$⊢\phi \to Y\in \mathrm{Old}\left(\mathrm{bday}\left(Z\right)\right)$$
19		breq1	$$⊢y=Y\to \left(y{<}_{s}Z\leftrightarrow Y{<}_{s}Z\right)$$
20		leftval	Could not format ( _Left ` Z ) = { y e. ( _Old ` ( bday ` Z ) ) | y
21	19 20	elrab2	Could not format ( Y e. ( _Left ` Z ) <-> ( Y e. ( _Old ` ( bday ` Z ) ) /\ Y ( Y e. ( _Old ` ( bday ` Z ) ) /\ Y
22	18 5 21	sylanbrc	Could not format ( ph -> Y e. ( _Left ` Z ) ) : No typesetting found for |- ( ph -> Y e. ( _Left ` Z ) ) with typecode |-
23		eqid	Could not format ( X +s Y ) = ( X +s Y ) : No typesetting found for |- ( X +s Y ) = ( X +s Y ) with typecode |-
24		oveq2	Could not format ( d = Y -> ( X +s d ) = ( X +s Y ) ) : No typesetting found for |- ( d = Y -> ( X +s d ) = ( X +s Y ) ) with typecode |-
25	24	rspceeqv	Could not format ( ( Y e. ( _Left ` Z ) /\ ( X +s Y ) = ( X +s Y ) ) -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) : No typesetting found for |- ( ( Y e. ( _Left ` Z ) /\ ( X +s Y ) = ( X +s Y ) ) -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) with typecode |-
26	22 23 25	sylancl	Could not format ( ph -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) : No typesetting found for |- ( ph -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) with typecode |-
27		ovex	Could not format ( X +s Y ) e. _V : No typesetting found for |- ( X +s Y ) e. _V with typecode |-
28		eqeq1	Could not format ( b = ( X +s Y ) -> ( b = ( X +s d ) <-> ( X +s Y ) = ( X +s d ) ) ) : No typesetting found for |- ( b = ( X +s Y ) -> ( b = ( X +s d ) <-> ( X +s Y ) = ( X +s d ) ) ) with typecode |-
29	28	rexbidv	Could not format ( b = ( X +s Y ) -> ( E. d e. ( _Left ` Z ) b = ( X +s d ) <-> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) ) : No typesetting found for |- ( b = ( X +s Y ) -> ( E. d e. ( _Left ` Z ) b = ( X +s d ) <-> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) ) with typecode |-
30	27 29	elab	Could not format ( ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } <-> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) : No typesetting found for |- ( ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } <-> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) with typecode |-
31	26 30	sylibr	Could not format ( ph -> ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) : No typesetting found for |- ( ph -> ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) with typecode |-
32		elun2	Could not format ( ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } -> ( X +s Y ) e. ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) ) : No typesetting found for |- ( ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } -> ( X +s Y ) e. ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) ) with typecode |-
33	31 32	syl	Could not format ( ph -> ( X +s Y ) e. ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) ) : No typesetting found for |- ( ph -> ( X +s Y ) e. ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) ) with typecode |-
34		ovex	Could not format ( X +s Z ) e. _V : No typesetting found for |- ( X +s Z ) e. _V with typecode |-
35	34	snid	Could not format ( X +s Z ) e. { ( X +s Z ) } : No typesetting found for |- ( X +s Z ) e. { ( X +s Z ) } with typecode |-
36	35	a1i	Could not format ( ph -> ( X +s Z ) e. { ( X +s Z ) } ) : No typesetting found for |- ( ph -> ( X +s Z ) e. { ( X +s Z ) } ) with typecode |-
37	14 33 36	ssltsepcd	Could not format ( ph -> ( X +s Y ) ( X +s Y )
38	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 |-
39	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 |-
40	37 38 39	3brtr4d	Could not format ( ph -> ( Y +s X ) ( Y +s X )