Theorem negsproplem4

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is simpler than B . (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	No typesetting found for |- ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
	negsproplem4.1	$$⊢\phi \to A\in \mathrm{No}$$
	negsproplem4.2	$$⊢\phi \to B\in \mathrm{No}$$
	negsproplem4.3	$$⊢\phi \to A{<}_{s}B$$
	negsproplem4.4	$$⊢\phi \to \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)$$
Assertion	negsproplem4	Could not format assertion : No typesetting found for |- ( ph -> ( -us ` B )

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	Could not format ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
2		negsproplem4.1	$$⊢\phi \to A\in \mathrm{No}$$
3		negsproplem4.2	$$⊢\phi \to B\in \mathrm{No}$$
4		negsproplem4.3	$$⊢\phi \to A{<}_{s}B$$
5		negsproplem4.4	$$⊢\phi \to \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)$$
6		uncom	$$⊢\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)=\mathrm{bday}\left(B\right)\cup \mathrm{bday}\left(A\right)$$
7	6	eleq2i	$$⊢\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(B\right)\cup \mathrm{bday}\left(A\right)\right)$$
8	7	imbi1i	Could not format ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
9	8	2ralbii	Could not format ( A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
10	1 9	sylib	Could not format ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
11	10 3	negsproplem3	Could not format ( ph -> ( ( -us ` B ) e. No /\ ( -us " ( _Right ` B ) ) < ( ( -us ` B ) e. No /\ ( -us " ( _Right ` B ) ) <
12	11	simp3d	Could not format ( ph -> { ( -us ` B ) } < { ( -us ` B ) } <
13		fvex	Could not format ( -us ` B ) e. _V : No typesetting found for |- ( -us ` B ) e. _V with typecode |-
14	13	snid	Could not format ( -us ` B ) e. { ( -us ` B ) } : No typesetting found for |- ( -us ` B ) e. { ( -us ` B ) } with typecode |-
15	14	a1i	Could not format ( ph -> ( -us ` B ) e. { ( -us ` B ) } ) : No typesetting found for |- ( ph -> ( -us ` B ) e. { ( -us ` B ) } ) with typecode |-
16		negsfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
17		leftssno	Could not format ( _Left ` B ) C_ No : No typesetting found for |- ( _Left ` B ) C_ No with typecode |-
18		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
19		oldbday	$$⊢\left(\mathrm{bday}\left(B\right)\in \mathrm{On}\wedge A\in \mathrm{No}\right)\to \left(A\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\leftrightarrow \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\right)$$
20	18 2 19	sylancr	$$⊢\phi \to \left(A\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\leftrightarrow \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\right)$$
21	5 20	mpbird	$$⊢\phi \to A\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
22		breq1	$$⊢a=A\to \left(a{<}_{s}B\leftrightarrow A{<}_{s}B\right)$$
23		leftval	Could not format ( _Left ` B ) = { a e. ( _Old ` ( bday ` B ) ) | a
24	22 23	elrab2	Could not format ( A e. ( _Left ` B ) <-> ( A e. ( _Old ` ( bday ` B ) ) /\ A ( A e. ( _Old ` ( bday ` B ) ) /\ A
25	21 4 24	sylanbrc	Could not format ( ph -> A e. ( _Left ` B ) ) : No typesetting found for |- ( ph -> A e. ( _Left ` B ) ) with typecode |-
26		fnfvima	Could not format ( ( -us Fn No /\ ( _Left ` B ) C_ No /\ A e. ( _Left ` B ) ) -> ( -us ` A ) e. ( -us " ( _Left ` B ) ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Left ` B ) C_ No /\ A e. ( _Left ` B ) ) -> ( -us ` A ) e. ( -us " ( _Left ` B ) ) ) with typecode |-
27	16 17 25 26	mp3an12i	Could not format ( ph -> ( -us ` A ) e. ( -us " ( _Left ` B ) ) ) : No typesetting found for |- ( ph -> ( -us ` A ) e. ( -us " ( _Left ` B ) ) ) with typecode |-
28	12 15 27	ssltsepcd	Could not format ( ph -> ( -us ` B ) ( -us ` B )