Theorem negsproplem6

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is the same age as B . (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
	negsproplem6.4	|- ( ph -> ( bday ` A ) = ( bday ` B ) )
Assertion	negsproplem6	|- ( 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		negsproplem6.4	|- ( ph -> ( bday ` A ) = ( bday ` B ) )
6		nodense	|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A E. d e. No ( ( bday ` d ) e. ( bday ` A ) /\ A
7	2 3 5 4 6	syl22anc	|- ( ph -> E. d e. No ( ( bday ` d ) e. ( bday ` A ) /\ A
8		uncom	|- ( ( bday ` A ) u. ( bday ` B ) ) = ( ( bday ` B ) u. ( bday ` A ) )
9	8	eleq2i	|- ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) <-> ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) )
10	9	imbi1i	|- ( ( ( ( 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 )
11	10	2ralbii	|- ( 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 )
12	1 11	sylib	|- ( 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 )
13	12 3	negsproplem3	|- ( ph -> ( ( -us ` B ) e. No /\ ( -us " ( _Right ` B ) ) <
14	13	simp1d	|- ( ph -> ( -us ` B ) e. No )
15	14	adantr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) e. No )
16	1	adantr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A 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 )
17		simprl	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. No )
18		0sno	|- 0s e. No
19	18	a1i	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A 0s e. No )
20		bday0s	|- ( bday ` 0s ) = (/)
21	20	uneq2i	|- ( ( bday ` d ) u. ( bday ` 0s ) ) = ( ( bday ` d ) u. (/) )
22		un0	|- ( ( bday ` d ) u. (/) ) = ( bday ` d )
23	21 22	eqtri	|- ( ( bday ` d ) u. ( bday ` 0s ) ) = ( bday ` d )
24		simprr1	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( bday ` d ) e. ( bday ` A ) )
25		elun1	|- ( ( bday ` d ) e. ( bday ` A ) -> ( bday ` d ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
26	24 25	syl	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( bday ` d ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
27	23 26	eqeltrid	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( ( bday ` d ) u. ( bday ` 0s ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) )
28	16 17 19 27	negsproplem1	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( ( -us ` d ) e. No /\ ( d ( -us ` 0s )
29	28	simpld	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. No )
30	1 2	negsproplem3	|- ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <
31	30	simp1d	|- ( ph -> ( -us ` A ) e. No )
32	31	adantr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` A ) e. No )
33	13	simp3d	|- ( ph -> { ( -us ` B ) } <
34	33	adantr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A { ( -us ` B ) } <
35		fvex	|- ( -us ` B ) e. _V
36	35	snid	|- ( -us ` B ) e. { ( -us ` B ) }
37	36	a1i	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) e. { ( -us ` B ) } )
38		negsfn	|- -us Fn No
39		leftssno	|- ( _Left ` B ) C_ No
40		bdayelon	|- ( bday ` A ) e. On
41		oldbday	|- ( ( ( bday ` A ) e. On /\ d e. No ) -> ( d e. ( _Old ` ( bday ` A ) ) <-> ( bday ` d ) e. ( bday ` A ) ) )
42	40 17 41	sylancr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( d e. ( _Old ` ( bday ` A ) ) <-> ( bday ` d ) e. ( bday ` A ) ) )
43	24 42	mpbird	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Old ` ( bday ` A ) ) )
44	5	fveq2d	|- ( ph -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` B ) ) )
45	44	adantr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` B ) ) )
46	43 45	eleqtrd	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Old ` ( bday ` B ) ) )
47		simprr3	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d
48		leftval	|- ( _Left ` B ) = { d e. ( _Old ` ( bday ` B ) ) | d
49	48	reqabi	|- ( d e. ( _Left ` B ) <-> ( d e. ( _Old ` ( bday ` B ) ) /\ d
50	46 47 49	sylanbrc	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Left ` B ) )
51		fnfvima	|- ( ( -us Fn No /\ ( _Left ` B ) C_ No /\ d e. ( _Left ` B ) ) -> ( -us ` d ) e. ( -us " ( _Left ` B ) ) )
52	38 39 50 51	mp3an12i	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. ( -us " ( _Left ` B ) ) )
53	34 37 52	ssltsepcd	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B )
54	30	simp2d	|- ( ph -> ( -us " ( _Right ` A ) ) <
55	54	adantr	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us " ( _Right ` A ) ) <
56		rightssno	|- ( _Right ` A ) C_ No
57		simprr2	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A A
58		rightval	|- ( _Right ` A ) = { d e. ( _Old ` ( bday ` A ) ) | A
59	58	reqabi	|- ( d e. ( _Right ` A ) <-> ( d e. ( _Old ` ( bday ` A ) ) /\ A
60	43 57 59	sylanbrc	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Right ` A ) )
61		fnfvima	|- ( ( -us Fn No /\ ( _Right ` A ) C_ No /\ d e. ( _Right ` A ) ) -> ( -us ` d ) e. ( -us " ( _Right ` A ) ) )
62	38 56 60 61	mp3an12i	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. ( -us " ( _Right ` A ) ) )
63		fvex	|- ( -us ` A ) e. _V
64	63	snid	|- ( -us ` A ) e. { ( -us ` A ) }
65	64	a1i	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` A ) e. { ( -us ` A ) } )
66	55 62 65	ssltsepcd	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d )
67	15 29 32 53 66	slttrd	|- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B )
68	7 67	rexlimddv	|- ( ph -> ( -us ` B )