Metamath Proof Explorer

Theorem addsproplem3

Description: Lemma for surreal addition properties. Show the cut properties of surreal addition. (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 )~~
		addsproplem2.2	$⊢ φ \to X \in No$
		addsproplem2.3	$⊢ φ \to Y \in No$
	Assertion	addsproplem3	Could not format assertion : No typesetting found for \|- ( ph -> ( ( X +s Y ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <

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		addsproplem2.2	$⊢ φ \to X \in No$
3		addsproplem2.3	$⊢ φ \to Y \in No$
4	1 2 3	addsproplem2	Could not format ( ph -> ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ~~( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <~~
5		scutcut	Could not format ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
6	4 5	syl	Could not format ( ph -> ( ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
7		addsval2	Could not format ( ( X e. No /\ Y e. No ) -> ( X +s Y ) = ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) ) : No typesetting found for \|- ( ( X e. No /\ Y e. No ) -> ( X +s Y ) = ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) ) with typecode \|-
8	2 3 7	syl2anc	Could not format ( ph -> ( X +s Y ) = ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) ) : No typesetting found for \|- ( ph -> ( X +s Y ) = ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) ) with typecode \|-
9	8	eleq1d	Could not format ( ph -> ( ( X +s Y ) e. No <-> ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No ) ) : No typesetting found for \|- ( ph -> ( ( X +s Y ) e. No <-> ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No ) ) with typecode \|-
10	8	sneqd	Could not format ( ph -> { ( X +s Y ) } = { ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) } ) : No typesetting found for \|- ( ph -> { ( X +s Y ) } = { ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) } ) with typecode \|-
11	10	breq2d	Could not format ( ph -> ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ~~( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <~~
12	10	breq1d	Could not format ( ph -> ( { ( X +s Y ) } < { ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) } < ( { ( X +s Y ) } < { ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) } <
13	9 11 12	3anbi123d	Could not format ( ph -> ( ( ( X +s Y ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( ( X +s Y ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) \|s ( { w \| E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t \| E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
14	6 13	mpbird	Could not format ( ph -> ( ( X +s Y ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ~~( ( X +s Y ) e. No /\ ( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <~~