Theorem addscutlem

Description: Lemma for addscut . Show the statement with some additional distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

	Ref	Expression
Hypotheses	addscutlem.1	$$⊢\phi \to X\in \mathrm{No}$$
	addscutlem.2	$$⊢\phi \to Y\in \mathrm{No}$$
Assertion	addscutlem	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		addscutlem.1	$$⊢\phi \to X\in \mathrm{No}$$
2		addscutlem.2	$$⊢\phi \to Y\in \mathrm{No}$$
3		addsprop	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( x +s y ) e. No /\ ( y ( y +s x )
4	3	a1d	Could not format ( ( x e. No /\ y e. No /\ 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 ` 0s ) ) ) -> ( ( 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 ` Y ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
5	4	rgen3	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 ` 0s ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( x +s y ) e. No /\ ( y ( y +s x )
6	5	a1i	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 ` 0s ) ) ) -> ( ( 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 ` 0s ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
7	6 1 2	addsproplem3	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 ) } ) <