Theorem bday0s

Description: Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	bday0s	Could not format assertion : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-0s	Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |-
2	1	fveq2i	Could not format ( bday ` 0s ) = ( bday ` ( (/) |s (/) ) ) : No typesetting found for |- ( bday ` 0s ) = ( bday ` ( (/) |s (/) ) ) with typecode |-
3		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
4		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
5		scutbday	$$⊢\varnothing {\ll }_s\varnothing \to \mathrm{bday}\left(\varnothing {|}_s\varnothing \right)=\bigcap \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}\right]$$
6	3 4 5	mp2b	$$⊢\mathrm{bday}\left(\varnothing {|}_s\varnothing \right)=\bigcap \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}\right]$$
7	2 6	eqtri	Could not format ( bday ` 0s ) = |^| ( bday " { x e. No | ( (/) <
8		snelpwi	$$⊢x\in \mathrm{No}\to \left\{x\right\}\in 𝒫\mathrm{No}$$
9		nulsslt	$$⊢\left\{x\right\}\in 𝒫\mathrm{No}\to \varnothing {\ll }_s\left\{x\right\}$$
10		nulssgt	$$⊢\left\{x\right\}\in 𝒫\mathrm{No}\to \left\{x\right\}{\ll }_s\varnothing$$
11	9 10	jca	$$⊢\left\{x\right\}\in 𝒫\mathrm{No}\to \left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)$$
12	8 11	syl	$$⊢x\in \mathrm{No}\to \left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)$$
13	12	rabeqc	$$⊢\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}=\mathrm{No}$$
14		bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$
15	13 14	eqtr4i	$$⊢\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}=\mathrm{dom}\mathrm{bday}$$
16	15	imaeq2i	$$⊢\mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}\right]=\mathrm{bday}\left[\mathrm{dom}\mathrm{bday}\right]$$
17		imadmrn	$$⊢\mathrm{bday}\left[\mathrm{dom}\mathrm{bday}\right]=\mathrm{ran}\mathrm{bday}$$
18		bdayrn	$$⊢\mathrm{ran}\mathrm{bday}=\mathrm{On}$$
19	16 17 18	3eqtri	$$⊢\mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}\right]=\mathrm{On}$$
20	19	inteqi	$$⊢\bigcap \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\right\}\right]=\bigcap \mathrm{On}$$
21		inton	$$⊢\bigcap \mathrm{On}=\varnothing$$
22	7 20 21	3eqtri	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-