Theorem old1

Description: The only surreal older than 1o is 0s . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	old1	$$⊢\mathrm{Old}\left(1_{𝑜}\right)=\left\{0_s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2		oldval	$$⊢1_{𝑜}\in \mathrm{On}\to \mathrm{Old}\left(1_{𝑜}\right)=\bigcup M\left[1_{𝑜}\right]$$
3	1 2	ax-mp	$$⊢\mathrm{Old}\left(1_{𝑜}\right)=\bigcup M\left[1_{𝑜}\right]$$
4		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
5	4	imaeq2i	$$⊢M\left[1_{𝑜}\right]=M\left[\left\{\varnothing \right\}\right]$$
6		madef	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}$$
7		ffn	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}\to MFn\mathrm{On}$$
8	6 7	ax-mp	$$⊢MFn\mathrm{On}$$
9		0elon	$$⊢\varnothing \in \mathrm{On}$$
10		fnsnfv	$$⊢\left(MFn\mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to \left\{M\left(\varnothing \right)\right\}=M\left[\left\{\varnothing \right\}\right]$$
11	8 9 10	mp2an	$$⊢\left\{M\left(\varnothing \right)\right\}=M\left[\left\{\varnothing \right\}\right]$$
12	5 11	eqtr4i	$$⊢M\left[1_{𝑜}\right]=\left\{M\left(\varnothing \right)\right\}$$
13	12	unieqi	$$⊢\bigcup M\left[1_{𝑜}\right]=\bigcup \left\{M\left(\varnothing \right)\right\}$$
14		fvex	$$⊢M\left(\varnothing \right)\in \mathrm{V}$$
15	14	unisn	$$⊢\bigcup \left\{M\left(\varnothing \right)\right\}=M\left(\varnothing \right)$$
16		made0	$$⊢M\left(\varnothing \right)=\left\{0_s\right\}$$
17	15 16	eqtri	$$⊢\bigcup \left\{M\left(\varnothing \right)\right\}=\left\{0_s\right\}$$
18	13 17	eqtri	$$⊢\bigcup M\left[1_{𝑜}\right]=\left\{0_s\right\}$$
19	3 18	eqtri	$$⊢\mathrm{Old}\left(1_{𝑜}\right)=\left\{0_s\right\}$$