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	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) ⊆ ( bday ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ ( -us ‘ 𝑥 ) ) = ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) )
2		fveq2	⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑥𝑂 ) )
3	1 2	sseq12d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ ( -us ‘ 𝑥 ) ) ⊆ ( bday ‘ 𝑥 ) ↔ ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) )
4		2fveq3	⊢ ( 𝑥 = 𝐴 → ( bday ‘ ( -us ‘ 𝑥 ) ) = ( bday ‘ ( -us ‘ 𝐴 ) ) )
5		fveq2	⊢ ( 𝑥 = 𝐴 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝐴 ) )
6	4 5	sseq12d	⊢ ( 𝑥 = 𝐴 → ( ( bday ‘ ( -us ‘ 𝑥 ) ) ⊆ ( bday ‘ 𝑥 ) ↔ ( bday ‘ ( -us ‘ 𝐴 ) ) ⊆ ( bday ‘ 𝐴 ) ) )
7		negsval	⊢ ( 𝑥 ∈ No → ( -us ‘ 𝑥 ) = ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) )
8	7	fveq2d	⊢ ( 𝑥 ∈ No → ( bday ‘ ( -us ‘ 𝑥 ) ) = ( bday ‘ ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) ) )
9	8	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ( bday ‘ ( -us ‘ 𝑥 ) ) = ( bday ‘ ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) ) )
10		negscut2	⊢ ( 𝑥 ∈ No → ( -us “ ( R ‘ 𝑥 ) ) <<s ( -us “ ( L ‘ 𝑥 ) ) )
11		lrold	⊢ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) = ( O ‘ ( bday ‘ 𝑥 ) )
12		uncom	⊢ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) = ( ( R ‘ 𝑥 ) ∪ ( L ‘ 𝑥 ) )
13	11 12	eqtr3i	⊢ ( O ‘ ( bday ‘ 𝑥 ) ) = ( ( R ‘ 𝑥 ) ∪ ( L ‘ 𝑥 ) )
14	13	imaeq2i	⊢ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) = ( -us “ ( ( R ‘ 𝑥 ) ∪ ( L ‘ 𝑥 ) ) )
15		imaundi	⊢ ( -us “ ( ( R ‘ 𝑥 ) ∪ ( L ‘ 𝑥 ) ) ) = ( ( -us “ ( R ‘ 𝑥 ) ) ∪ ( -us “ ( L ‘ 𝑥 ) ) )
16	14 15	eqtri	⊢ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) = ( ( -us “ ( R ‘ 𝑥 ) ) ∪ ( -us “ ( L ‘ 𝑥 ) ) )
17	16	imaeq2i	⊢ ( bday “ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) = ( bday “ ( ( -us “ ( R ‘ 𝑥 ) ) ∪ ( -us “ ( L ‘ 𝑥 ) ) ) )
18	11	raleqi	⊢ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ↔ ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) )
19		oldbdayim	⊢ ( 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) → ( bday ‘ 𝑥𝑂 ) ∈ ( bday ‘ 𝑥 ) )
20	19	adantl	⊢ ( ( 𝑥 ∈ No ∧ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ) → ( bday ‘ 𝑥𝑂 ) ∈ ( bday ‘ 𝑥 ) )
21		bdayelon	⊢ ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ On
22		bdayelon	⊢ ( bday ‘ 𝑥 ) ∈ On
23		ontr2	⊢ ( ( ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ On ∧ ( bday ‘ 𝑥 ) ∈ On ) → ( ( ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ∧ ( bday ‘ 𝑥𝑂 ) ∈ ( bday ‘ 𝑥 ) ) → ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) ) )
24	21 22 23	mp2an	⊢ ( ( ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ∧ ( bday ‘ 𝑥𝑂 ) ∈ ( bday ‘ 𝑥 ) ) → ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) )
25	24	a1i	⊢ ( ( 𝑥 ∈ No ∧ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ) → ( ( ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ∧ ( bday ‘ 𝑥𝑂 ) ∈ ( bday ‘ 𝑥 ) ) → ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) ) )
26	20 25	mpan2d	⊢ ( ( 𝑥 ∈ No ∧ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ) → ( ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) → ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) ) )
27	26	ralimdva	⊢ ( 𝑥 ∈ No → ( ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) → ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) ) )
28	27	imp	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) )
29		bdayfun	⊢ Fun bday
30		imassrn	⊢ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ⊆ ran -us
31		bdaydm	⊢ dom bday = No
32		negsfo	⊢ -us : No –onto→ No
33		forn	⊢ ( -us : No –onto→ No → ran -us = No )
34	32 33	ax-mp	⊢ ran -us = No
35	31 34	eqtr4i	⊢ dom bday = ran -us
36	30 35	sseqtrri	⊢ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ⊆ dom bday
37		funimass4	⊢ ( ( Fun bday ∧ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ⊆ dom bday ) → ( ( bday “ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝑥 ) ) )
38	29 36 37	mp2an	⊢ ( ( bday “ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝑥 ) )
39		negsfn	⊢ -us Fn No
40		oldssno	⊢ ( O ‘ ( bday ‘ 𝑥 ) ) ⊆ No
41		fveq2	⊢ ( 𝑦 = ( -us ‘ 𝑥𝑂 ) → ( bday ‘ 𝑦 ) = ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) )
42	41	eleq1d	⊢ ( 𝑦 = ( -us ‘ 𝑥𝑂 ) → ( ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝑥 ) ↔ ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) ) )
43	42	ralima	⊢ ( ( -us Fn No ∧ ( O ‘ ( bday ‘ 𝑥 ) ) ⊆ No ) → ( ∀ 𝑦 ∈ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝑥 ) ↔ ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) ) )
44	39 40 43	mp2an	⊢ ( ∀ 𝑦 ∈ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝑥 ) ↔ ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) )
45	38 44	bitri	⊢ ( ( bday “ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) ↔ ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ∈ ( bday ‘ 𝑥 ) )
46	28 45	sylibr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ( bday “ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) )
47	18 46	sylan2b	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ( bday “ ( -us “ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) )
48	17 47	eqsstrrid	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ( bday “ ( ( -us “ ( R ‘ 𝑥 ) ) ∪ ( -us “ ( L ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) )
49		scutbdaybnd	⊢ ( ( ( -us “ ( R ‘ 𝑥 ) ) <<s ( -us “ ( L ‘ 𝑥 ) ) ∧ ( bday ‘ 𝑥 ) ∈ On ∧ ( bday “ ( ( -us “ ( R ‘ 𝑥 ) ) ∪ ( -us “ ( L ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) ) → ( bday ‘ ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) )
50	22 49	mp3an2	⊢ ( ( ( -us “ ( R ‘ 𝑥 ) ) <<s ( -us “ ( L ‘ 𝑥 ) ) ∧ ( bday “ ( ( -us “ ( R ‘ 𝑥 ) ) ∪ ( -us “ ( L ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) ) → ( bday ‘ ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) )
51	10 48 50	syl2an2r	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ( bday ‘ ( ( -us “ ( R ‘ 𝑥 ) ) |s ( -us “ ( L ‘ 𝑥 ) ) ) ) ⊆ ( bday ‘ 𝑥 ) )
52	9 51	eqsstrd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) ) → ( bday ‘ ( -us ‘ 𝑥 ) ) ⊆ ( bday ‘ 𝑥 ) )
53	52	ex	⊢ ( 𝑥 ∈ No → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( -us ‘ 𝑥𝑂 ) ) ⊆ ( bday ‘ 𝑥𝑂 ) → ( bday ‘ ( -us ‘ 𝑥 ) ) ⊆ ( bday ‘ 𝑥 ) ) )
54	3 6 53	noinds	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) ⊆ ( bday ‘ 𝐴 ) )