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	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)\subseteq \mathrm{bday}\left(A\right)$$

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	$$⊢x=A\to \mathrm{bday}\left({+}_s\left(x\right)\right)=\mathrm{bday}\left({+}_s\left(A\right)\right)$$
5		fveq2	$$⊢x=A\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(A\right)$$
6	4 5	sseq12d	$$⊢x=A\to \left(\mathrm{bday}\left({+}_s\left(x\right)\right)\subseteq \mathrm{bday}\left(x\right)\leftrightarrow \mathrm{bday}\left({+}_s\left(A\right)\right)\subseteq \mathrm{bday}\left(A\right)\right)$$
7		negsval	$$⊢x\in \mathrm{No}\to {+}_s\left(x\right)={+}_s\left[R\left(x\right)\right]{|}_s{+}_s\left[L\left(x\right)\right]$$
8	7	fveq2d	$$⊢x\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(x\right)\right)=\mathrm{bday}\left({+}_s\left[R\left(x\right)\right]{|}_s{+}_s\left[L\left(x\right)\right]\right)$$
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	$$⊢x\in \mathrm{No}\to {+}_s\left[R\left(x\right)\right]{\ll }_s{+}_s\left[L\left(x\right)\right]$$
11		lrold	$$⊢L\left(x\right)\cup R\left(x\right)=\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)$$
12		uncom	$$⊢L\left(x\right)\cup R\left(x\right)=R\left(x\right)\cup L\left(x\right)$$
13	11 12	eqtr3i	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)=R\left(x\right)\cup L\left(x\right)$$
14	13	imaeq2i	$$⊢{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]={+}_s\left[R\left(x\right)\cup L\left(x\right)\right]$$
15		imaundi	$$⊢{+}_s\left[R\left(x\right)\cup L\left(x\right)\right]={+}_s\left[R\left(x\right)\right]\cup {+}_s\left[L\left(x\right)\right]$$
16	14 15	eqtri	$$⊢{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]={+}_s\left[R\left(x\right)\right]\cup {+}_s\left[L\left(x\right)\right]$$
17	16	imaeq2i	$$⊢\mathrm{bday}\left[{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\right]=\mathrm{bday}\left[{+}_s\left[R\left(x\right)\right]\cup {+}_s\left[L\left(x\right)\right]\right]$$
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	$$⊢{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\subseteq \mathrm{ran}{+}_s$$
31		bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$
32		negsfo	$$⊢{+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}$$
33		forn	$$⊢{+}_s:\mathrm{No}\underset{onto}{⟶}\mathrm{No}\to \mathrm{ran}{+}_s=\mathrm{No}$$
34	32 33	ax-mp	$$⊢\mathrm{ran}{+}_s=\mathrm{No}$$
35	31 34	eqtr4i	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{ran}{+}_s$$
36	30 35	sseqtrri	$$⊢{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\subseteq \mathrm{dom}\mathrm{bday}$$
37		funimass4	$$⊢\left(\mathrm{Fun}\mathrm{bday}\wedge {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\subseteq \mathrm{dom}\mathrm{bday}\right)\to \left(\mathrm{bday}\left[{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\right]\subseteq \mathrm{bday}\left(x\right)\leftrightarrow \forall y\in {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x\right)\right)$$
38	29 36 37	mp2an	$$⊢\mathrm{bday}\left[{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\right]\subseteq \mathrm{bday}\left(x\right)\leftrightarrow \forall y\in {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)\right]\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x\right)$$
39		negsfn	$$⊢{+}_{s}Fn\mathrm{No}$$
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	$$⊢\left({+}_s\left[R\left(x\right)\right]{\ll }_s{+}_s\left[L\left(x\right)\right]\wedge \mathrm{bday}\left(x\right)\in \mathrm{On}\wedge \mathrm{bday}\left[{+}_s\left[R\left(x\right)\right]\cup {+}_s\left[L\left(x\right)\right]\right]\subseteq \mathrm{bday}\left(x\right)\right)\to \mathrm{bday}\left({+}_s\left[R\left(x\right)\right]{|}_s{+}_s\left[L\left(x\right)\right]\right)\subseteq \mathrm{bday}\left(x\right)$$
50	22 49	mp3an2	$$⊢\left({+}_s\left[R\left(x\right)\right]{\ll }_s{+}_s\left[L\left(x\right)\right]\wedge \mathrm{bday}\left[{+}_s\left[R\left(x\right)\right]\cup {+}_s\left[L\left(x\right)\right]\right]\subseteq \mathrm{bday}\left(x\right)\right)\to \mathrm{bday}\left({+}_s\left[R\left(x\right)\right]{|}_s{+}_s\left[L\left(x\right)\right]\right)\subseteq \mathrm{bday}\left(x\right)$$
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	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)\subseteq \mathrm{bday}\left(A\right)$$