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	|- ( 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	|- ( ph -> A e. No )
	negsproplem4.2	|- ( ph -> B e. No )
	negsproplem4.3	|- ( ph -> A
	negsproplem5.4	|- ( ph -> ( bday ` B ) e. ( bday ` A ) )
Assertion	negsproplem5	|- ( ph -> ( -us ` B )

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	|- ( 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 )
2		negsproplem4.1	|- ( ph -> A e. No )
3		negsproplem4.2	|- ( ph -> B e. No )
4		negsproplem4.3	|- ( ph -> A
5		negsproplem5.4	|- ( ph -> ( bday ` B ) e. ( bday ` A ) )
6	1 2	negsproplem3	|- ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <
7	6	simp2d	|- ( ph -> ( -us " ( _Right ` A ) ) <
8		negsfn	|- -us Fn No
9		rightssno	|- ( _Right ` A ) C_ No
10		bdayelon	|- ( bday ` A ) e. On
11		oldbday	|- ( ( ( bday ` A ) e. On /\ B e. No ) -> ( B e. ( _Old ` ( bday ` A ) ) <-> ( bday ` B ) e. ( bday ` A ) ) )
12	10 3 11	sylancr	|- ( ph -> ( B e. ( _Old ` ( bday ` A ) ) <-> ( bday ` B ) e. ( bday ` A ) ) )
13	5 12	mpbird	|- ( ph -> B e. ( _Old ` ( bday ` A ) ) )
14		breq2	|- ( b = B -> ( A A
15		rightval	|- ( _Right ` A ) = { b e. ( _Old ` ( bday ` A ) ) | A
16	14 15	elrab2	|- ( B e. ( _Right ` A ) <-> ( B e. ( _Old ` ( bday ` A ) ) /\ A
17	13 4 16	sylanbrc	|- ( ph -> B e. ( _Right ` A ) )
18		fnfvima	|- ( ( -us Fn No /\ ( _Right ` A ) C_ No /\ B e. ( _Right ` A ) ) -> ( -us ` B ) e. ( -us " ( _Right ` A ) ) )
19	8 9 17 18	mp3an12i	|- ( ph -> ( -us ` B ) e. ( -us " ( _Right ` A ) ) )
20		fvex	|- ( -us ` A ) e. _V
21	20	snid	|- ( -us ` A ) e. { ( -us ` A ) }
22	21	a1i	|- ( ph -> ( -us ` A ) e. { ( -us ` A ) } )
23	7 19 22	ssltsepcd	|- ( ph -> ( -us ` B )