Metamath Proof Explorer

Theorem addscut2

Description: Show that the cut involved in surreal addition is legitimate. (Contributed by Scott Fenton, 8-Mar-2025)

		Ref	Expression
	Hypotheses	addscut.1	$⊢ φ \to X \in No$
		addscut.2	$⊢ φ \to Y \in No$
	Assertion	addscut2	Could not format assertion : No typesetting found for \|- ( ph -> ( { 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		addscut.1	$⊢ φ \to X \in No$
2		addscut.2	$⊢ φ \to Y \in No$
3	1 2	addscut	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 ) } ) <~~
4		3anass	Could not format ( ( ( 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 ) } ) < ~~( ( 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 ) } ) <~~
5	3 4	sylib	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 ) } ) <~~
6	5	simprd	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 ) } ) <~~
7		ovex	Could not format ( X +s Y ) e. _V : No typesetting found for \|- ( X +s Y ) e. _V with typecode \|-
8	7	snnz	Could not format { ( X +s Y ) } =/= (/) : No typesetting found for \|- { ( X +s Y ) } =/= (/) with typecode \|-
9		sslttr	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 ) } ) < ~~( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <~~
10	8 9	mp3an3	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 ) } ) < ~~( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <~~
11	6 10	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 ) } ) < ~~( { p \| E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q \| E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <~~