Theorem negsbdaylem

Description: Lemma for negsbday . Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025)

	Ref	Expression
Assertion	negsbdaylem	Could not format assertion : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2fveq3	Could not format ( x = xO -> ( bday ` ( -us ` x ) ) = ( bday ` ( -us ` xO ) ) ) : No typesetting found for |- ( x = xO -> ( bday ` ( -us ` x ) ) = ( bday ` ( -us ` xO ) ) ) with typecode |-
2		fveq2	Could not format ( x = xO -> ( bday ` x ) = ( bday ` xO ) ) : No typesetting found for |- ( x = xO -> ( bday ` x ) = ( bday ` xO ) ) with typecode |-
3	1 2	sseq12d	Could not format ( x = xO -> ( ( bday ` ( -us ` x ) ) C_ ( bday ` x ) <-> ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` ( -us ` x ) ) C_ ( bday ` x ) <-> ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) ) with typecode |-
4		2fveq3	Could not format ( x = A -> ( bday ` ( -us ` x ) ) = ( bday ` ( -us ` A ) ) ) : No typesetting found for |- ( x = A -> ( bday ` ( -us ` x ) ) = ( bday ` ( -us ` A ) ) ) with typecode |-
5		fveq2	$$⊢x=A\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(A\right)$$
6	4 5	sseq12d	Could not format ( x = A -> ( ( bday ` ( -us ` x ) ) C_ ( bday ` x ) <-> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) ) : No typesetting found for |- ( x = A -> ( ( bday ` ( -us ` x ) ) C_ ( bday ` x ) <-> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) ) with typecode |-
7		negsval	Could not format ( x e. No -> ( -us ` x ) = ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) : No typesetting found for |- ( x e. No -> ( -us ` x ) = ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) with typecode |-
8	7	fveq2d	Could not format ( x e. No -> ( bday ` ( -us ` x ) ) = ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) ) : No typesetting found for |- ( x e. No -> ( bday ` ( -us ` x ) ) = ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) ) with typecode |-
9	8	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( -us ` x ) ) = ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( -us ` x ) ) = ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) ) with typecode |-
10		negscut2	Could not format ( x e. No -> ( -us " ( _Right ` x ) ) < ( -us " ( _Right ` x ) ) <
11		lrold	Could not format ( ( _Left ` x ) u. ( _Right ` x ) ) = ( _Old ` ( bday ` x ) ) : No typesetting found for |- ( ( _Left ` x ) u. ( _Right ` x ) ) = ( _Old ` ( bday ` x ) ) with typecode |-
12		uncom	Could not format ( ( _Left ` x ) u. ( _Right ` x ) ) = ( ( _Right ` x ) u. ( _Left ` x ) ) : No typesetting found for |- ( ( _Left ` x ) u. ( _Right ` x ) ) = ( ( _Right ` x ) u. ( _Left ` x ) ) with typecode |-
13	11 12	eqtr3i	Could not format ( _Old ` ( bday ` x ) ) = ( ( _Right ` x ) u. ( _Left ` x ) ) : No typesetting found for |- ( _Old ` ( bday ` x ) ) = ( ( _Right ` x ) u. ( _Left ` x ) ) with typecode |-
14	13	imaeq2i	Could not format ( -us " ( _Old ` ( bday ` x ) ) ) = ( -us " ( ( _Right ` x ) u. ( _Left ` x ) ) ) : No typesetting found for |- ( -us " ( _Old ` ( bday ` x ) ) ) = ( -us " ( ( _Right ` x ) u. ( _Left ` x ) ) ) with typecode |-
15		imaundi	Could not format ( -us " ( ( _Right ` x ) u. ( _Left ` x ) ) ) = ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) : No typesetting found for |- ( -us " ( ( _Right ` x ) u. ( _Left ` x ) ) ) = ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) with typecode |-
16	14 15	eqtri	Could not format ( -us " ( _Old ` ( bday ` x ) ) ) = ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) : No typesetting found for |- ( -us " ( _Old ` ( bday ` x ) ) ) = ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) with typecode |-
17	16	imaeq2i	Could not format ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) = ( bday " ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) ) : No typesetting found for |- ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) = ( bday " ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) ) with typecode |-
18	11	raleqi	Could not format ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) : No typesetting found for |- ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) with typecode |-
19		oldbdayim	Could not format ( xO e. ( _Old ` ( bday ` x ) ) -> ( bday ` xO ) e. ( bday ` x ) ) : No typesetting found for |- ( xO e. ( _Old ` ( bday ` x ) ) -> ( bday ` xO ) e. ( bday ` x ) ) with typecode |-
20	19	adantl	Could not format ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( bday ` xO ) e. ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( bday ` xO ) e. ( bday ` x ) ) with typecode |-
21		bdayelon	Could not format ( bday ` ( -us ` xO ) ) e. On : No typesetting found for |- ( bday ` ( -us ` xO ) ) e. On with typecode |-
22		bdayelon	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{On}$$
23		ontr2	Could not format ( ( ( bday ` ( -us ` xO ) ) e. On /\ ( bday ` x ) e. On ) -> ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) : No typesetting found for |- ( ( ( bday ` ( -us ` xO ) ) e. On /\ ( bday ` x ) e. On ) -> ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) with typecode |-
24	21 22 23	mp2an	Could not format ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) : No typesetting found for |- ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) with typecode |-
25	24	a1i	Could not format ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) with typecode |-
26	20 25	mpan2d	Could not format ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) with typecode |-
27	26	ralimdva	Could not format ( x e. No -> ( A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) : No typesetting found for |- ( x e. No -> ( A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) with typecode |-
28	27	imp	Could not format ( ( x e. No /\ A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) with typecode |-
29		bdayfun	$$⊢\mathrm{Fun}\mathrm{bday}$$
30		imassrn	Could not format ( -us " ( _Old ` ( bday ` x ) ) ) C_ ran -us : No typesetting found for |- ( -us " ( _Old ` ( bday ` x ) ) ) C_ ran -us with typecode |-
31		bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$
32		negsfo	Could not format -us : No -onto-> No : No typesetting found for |- -us : No -onto-> No with typecode |-
33		forn	Could not format ( -us : No -onto-> No -> ran -us = No ) : No typesetting found for |- ( -us : No -onto-> No -> ran -us = No ) with typecode |-
34	32 33	ax-mp	Could not format ran -us = No : No typesetting found for |- ran -us = No with typecode |-
35	31 34	eqtr4i	Could not format dom bday = ran -us : No typesetting found for |- dom bday = ran -us with typecode |-
36	30 35	sseqtrri	Could not format ( -us " ( _Old ` ( bday ` x ) ) ) C_ dom bday : No typesetting found for |- ( -us " ( _Old ` ( bday ` x ) ) ) C_ dom bday with typecode |-
37		funimass4	Could not format ( ( Fun bday /\ ( -us " ( _Old ` ( bday ` x ) ) ) C_ dom bday ) -> ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) ) ) : No typesetting found for |- ( ( Fun bday /\ ( -us " ( _Old ` ( bday ` x ) ) ) C_ dom bday ) -> ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) ) ) with typecode |-
38	29 36 37	mp2an	Could not format ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) ) : No typesetting found for |- ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) ) with typecode |-
39		negsfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
40		oldssno	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\subseteq \mathrm{No}$$
41		fveq2	Could not format ( y = ( -us ` xO ) -> ( bday ` y ) = ( bday ` ( -us ` xO ) ) ) : No typesetting found for |- ( y = ( -us ` xO ) -> ( bday ` y ) = ( bday ` ( -us ` xO ) ) ) with typecode |-
42	41	eleq1d	Could not format ( y = ( -us ` xO ) -> ( ( bday ` y ) e. ( bday ` x ) <-> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) : No typesetting found for |- ( y = ( -us ` xO ) -> ( ( bday ` y ) e. ( bday ` x ) <-> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) with typecode |-
43	42	imaeqsalv	Could not format ( ( -us Fn No /\ ( _Old ` ( bday ` x ) ) C_ No ) -> ( A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Old ` ( bday ` x ) ) C_ No ) -> ( A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) ) with typecode |-
44	39 40 43	mp2an	Could not format ( A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) : No typesetting found for |- ( A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) with typecode |-
45	38 44	bitri	Could not format ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) : No typesetting found for |- ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) with typecode |-
46	28 45	sylibr	Could not format ( ( x e. No /\ A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) ) with typecode |-
47	18 46	sylan2b	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) ) with typecode |-
48	17 47	eqsstrrid	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) with typecode |-
49		scutbdaybnd	Could not format ( ( ( -us " ( _Right ` x ) ) < ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( ( -us " ( _Right ` x ) ) < ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) with typecode |-
50	22 49	mp3an2	Could not format ( ( ( -us " ( _Right ` x ) ) < ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( ( -us " ( _Right ` x ) ) < ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) with typecode |-
51	10 48 50	syl2an2r	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) ) with typecode |-
52	9 51	eqsstrd	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( -us ` x ) ) C_ ( bday ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( -us ` x ) ) C_ ( bday ` x ) ) with typecode |-
53	52	ex	Could not format ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> ( bday ` ( -us ` x ) ) C_ ( bday ` x ) ) ) : No typesetting found for |- ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> ( bday ` ( -us ` x ) ) C_ ( bday ` x ) ) ) with typecode |-
54	3 6 53	noinds	Could not format ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) : No typesetting found for |- ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) with typecode |-