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	Could not format _Old = ( x e. On |-> U. ( _Made " x ) ) : No typesetting found for |- _Old = ( x e. On |-> U. ( _Made " x ) ) with typecode |-
2		imassrn	Could not format ( _Made " x ) C_ ran _Made : No typesetting found for |- ( _Made " x ) C_ ran _Made with typecode |-
3		madef	Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
4		frn	Could not format ( _Made : On --> ~P No -> ran _Made C_ ~P No ) : No typesetting found for |- ( _Made : On --> ~P No -> ran _Made C_ ~P No ) with typecode |-
5	3 4	ax-mp	Could not format ran _Made C_ ~P No : No typesetting found for |- ran _Made C_ ~P No with typecode |-
6	2 5	sstri	Could not format ( _Made " x ) C_ ~P No : No typesetting found for |- ( _Made " x ) C_ ~P No with typecode |-
7	6	sseli	Could not format ( y e. ( _Made " x ) -> y e. ~P No ) : No typesetting found for |- ( y e. ( _Made " x ) -> y e. ~P No ) with typecode |-
8	7	elpwid	Could not format ( y e. ( _Made " x ) -> y C_ No ) : No typesetting found for |- ( y e. ( _Made " x ) -> y C_ No ) with typecode |-
9	8	rgen	Could not format A. y e. ( _Made " x ) y C_ No : No typesetting found for |- A. y e. ( _Made " x ) y C_ No with typecode |-
10	9	a1i	Could not format ( x e. On -> A. y e. ( _Made " x ) y C_ No ) : No typesetting found for |- ( x e. On -> A. y e. ( _Made " x ) y C_ No ) with typecode |-
11		ffun	Could not format ( _Made : On --> ~P No -> Fun _Made ) : No typesetting found for |- ( _Made : On --> ~P No -> Fun _Made ) with typecode |-
12	3 11	ax-mp	Could not format Fun _Made : No typesetting found for |- Fun _Made with typecode |-
13		vex	$$⊢x\in \mathrm{V}$$
14	13	funimaex	Could not format ( Fun _Made -> ( _Made " x ) e. _V ) : No typesetting found for |- ( Fun _Made -> ( _Made " x ) e. _V ) with typecode |-
15	12 14	ax-mp	Could not format ( _Made " x ) e. _V : No typesetting found for |- ( _Made " x ) e. _V with typecode |-
16	15	uniex	Could not format U. ( _Made " x ) e. _V : No typesetting found for |- U. ( _Made " x ) e. _V with typecode |-
17	16	elpw	Could not format ( U. ( _Made " x ) e. ~P No <-> U. ( _Made " x ) C_ No ) : No typesetting found for |- ( U. ( _Made " x ) e. ~P No <-> U. ( _Made " x ) C_ No ) with typecode |-
18		unissb	Could not format ( U. ( _Made " x ) C_ No <-> A. y e. ( _Made " x ) y C_ No ) : No typesetting found for |- ( U. ( _Made " x ) C_ No <-> A. y e. ( _Made " x ) y C_ No ) with typecode |-
19	17 18	bitri	Could not format ( U. ( _Made " x ) e. ~P No <-> A. y e. ( _Made " x ) y C_ No ) : No typesetting found for |- ( U. ( _Made " x ) e. ~P No <-> A. y e. ( _Made " x ) y C_ No ) with typecode |-
20	10 19	sylibr	Could not format ( x e. On -> U. ( _Made " x ) e. ~P No ) : No typesetting found for |- ( x e. On -> U. ( _Made " x ) e. ~P No ) with typecode |-
21	1 20	fmpti	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$