Theorem addsproplem5

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