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	|- _Old : On --> ~P No

Proof

Step	Hyp	Ref	Expression
1		df-old	|- _Old = ( x e. On |-> U. ( _M " x ) )
2		imassrn	|- ( _M " x ) C_ ran _M
3		madef	|- _M : On --> ~P No
4		frn	|- ( _M : On --> ~P No -> ran _M C_ ~P No )
5	3 4	ax-mp	|- ran _M C_ ~P No
6	2 5	sstri	|- ( _M " x ) C_ ~P No
7	6	sseli	|- ( y e. ( _M " x ) -> y e. ~P No )
8	7	elpwid	|- ( y e. ( _M " x ) -> y C_ No )
9	8	rgen	|- A. y e. ( _M " x ) y C_ No
10	9	a1i	|- ( x e. On -> A. y e. ( _M " x ) y C_ No )
11		ffun	|- ( _M : On --> ~P No -> Fun _M )
12	3 11	ax-mp	|- Fun _M
13		vex	|- x e. _V
14	13	funimaex	|- ( Fun _M -> ( _M " x ) e. _V )
15	12 14	ax-mp	|- ( _M " x ) e. _V
16	15	uniex	|- U. ( _M " x ) e. _V
17	16	elpw	|- ( U. ( _M " x ) e. ~P No <-> U. ( _M " x ) C_ No )
18		unissb	|- ( U. ( _M " x ) C_ No <-> A. y e. ( _M " x ) y C_ No )
19	17 18	bitri	|- ( U. ( _M " x ) e. ~P No <-> A. y e. ( _M " x ) y C_ No )
20	10 19	sylibr	|- ( x e. On -> U. ( _M " x ) e. ~P No )
21	1 20	fmpti	|- _Old : On --> ~P No