Theorem negsproplem5

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when B is simpler than A . (Contributed by Scott Fenton, 3-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$$
	negsproplem5.4	$$⊢\phi \to \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)$$
Assertion	negsproplem5	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		negsproplem5.4	$$⊢\phi \to \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)$$
6	1 2	negsproplem3	Could not format ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <
7	6	simp2d	Could not format ( ph -> ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
8		negsfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
9		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
10		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
11		oldbday	$$⊢\left(\mathrm{bday}\left(A\right)\in \mathrm{On}\wedge B\in \mathrm{No}\right)\to \left(B\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\leftrightarrow \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)$$
12	10 3 11	sylancr	$$⊢\phi \to \left(B\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\leftrightarrow \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)$$
13	5 12	mpbird	$$⊢\phi \to B\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
14		breq2	$$⊢b=B\to \left(A{<}_{s}b\leftrightarrow A{<}_{s}B\right)$$
15		rightval	Could not format ( _Right ` A ) = { b e. ( _Old ` ( bday ` A ) ) | A
16	14 15	elrab2	Could not format ( B e. ( _Right ` A ) <-> ( B e. ( _Old ` ( bday ` A ) ) /\ A ( B e. ( _Old ` ( bday ` A ) ) /\ A
17	13 4 16	sylanbrc	Could not format ( ph -> B e. ( _Right ` A ) ) : No typesetting found for |- ( ph -> B e. ( _Right ` A ) ) with typecode |-
18		fnfvima	Could not format ( ( -us Fn No /\ ( _Right ` A ) C_ No /\ B e. ( _Right ` A ) ) -> ( -us ` B ) e. ( -us " ( _Right ` A ) ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Right ` A ) C_ No /\ B e. ( _Right ` A ) ) -> ( -us ` B ) e. ( -us " ( _Right ` A ) ) ) with typecode |-
19	8 9 17 18	mp3an12i	Could not format ( ph -> ( -us ` B ) e. ( -us " ( _Right ` A ) ) ) : No typesetting found for |- ( ph -> ( -us ` B ) e. ( -us " ( _Right ` A ) ) ) with typecode |-
20		fvex	Could not format ( -us ` A ) e. _V : No typesetting found for |- ( -us ` A ) e. _V with typecode |-
21	20	snid	Could not format ( -us ` A ) e. { ( -us ` A ) } : No typesetting found for |- ( -us ` A ) e. { ( -us ` A ) } with typecode |-
22	21	a1i	Could not format ( ph -> ( -us ` A ) e. { ( -us ` A ) } ) : No typesetting found for |- ( ph -> ( -us ` A ) e. { ( -us ` A ) } ) with typecode |-
23	7 19 22	ssltsepcd	Could not format ( ph -> ( -us ` B ) ( -us ` B )