Theorem oldf

Description: The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	oldf	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		df-old	$$⊢\mathrm{Old}=\left(x\in \mathrm{On}⟼\bigcup M\left[x\right]\right)$$
2		imassrn	$$⊢M\left[x\right]\subseteq \mathrm{ran}M$$
3		madef	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}$$
4		frn	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}\to \mathrm{ran}M\subseteq 𝒫\mathrm{No}$$
5	3 4	ax-mp	$$⊢\mathrm{ran}M\subseteq 𝒫\mathrm{No}$$
6	2 5	sstri	$$⊢M\left[x\right]\subseteq 𝒫\mathrm{No}$$
7	6	sseli	$$⊢y\in M\left[x\right]\to y\in 𝒫\mathrm{No}$$
8	7	elpwid	$$⊢y\in M\left[x\right]\to y\subseteq \mathrm{No}$$
9	8	rgen	$$⊢\forall y\in M\left[x\right]y\subseteq \mathrm{No}$$
10	9	a1i	$$⊢x\in \mathrm{On}\to \forall y\in M\left[x\right]y\subseteq \mathrm{No}$$
11		ffun	$$⊢M:\mathrm{On}⟶𝒫\mathrm{No}\to \mathrm{Fun}M$$
12	3 11	ax-mp	$$⊢\mathrm{Fun}M$$
13		vex	$$⊢x\in \mathrm{V}$$
14	13	funimaex	$$⊢\mathrm{Fun}M\to M\left[x\right]\in \mathrm{V}$$
15	12 14	ax-mp	$$⊢M\left[x\right]\in \mathrm{V}$$
16	15	uniex	$$⊢\bigcup M\left[x\right]\in \mathrm{V}$$
17	16	elpw	$$⊢\bigcup M\left[x\right]\in 𝒫\mathrm{No}\leftrightarrow \bigcup M\left[x\right]\subseteq \mathrm{No}$$
18		unissb	$$⊢\bigcup M\left[x\right]\subseteq \mathrm{No}\leftrightarrow \forall y\in M\left[x\right]y\subseteq \mathrm{No}$$
19	17 18	bitri	$$⊢\bigcup M\left[x\right]\in 𝒫\mathrm{No}\leftrightarrow \forall y\in M\left[x\right]y\subseteq \mathrm{No}$$
20	10 19	sylibr	$$⊢x\in \mathrm{On}\to \bigcup M\left[x\right]\in 𝒫\mathrm{No}$$
21	1 20	fmpti	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$