Theorem newf

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

	Ref	Expression
Assertion	newf	|- _New : On --> ~P No

Proof

Step	Hyp	Ref	Expression
1		df-new	|- _New = ( x e. On |-> ( ( _Made ` x ) \ ( _Old ` x ) ) )
2		madef	|- _Made : On --> ~P No
3	2	ffvelcdmi	|- ( x e. On -> ( _Made ` x ) e. ~P No )
4	3	elpwid	|- ( x e. On -> ( _Made ` x ) C_ No )
5	4	ssdifssd	|- ( x e. On -> ( ( _Made ` x ) \ ( _Old ` x ) ) C_ No )
6		fvex	|- ( _Made ` x ) e. _V
7	6	difexi	|- ( ( _Made ` x ) \ ( _Old ` x ) ) e. _V
8	7	elpw	|- ( ( ( _Made ` x ) \ ( _Old ` x ) ) e. ~P No <-> ( ( _Made ` x ) \ ( _Old ` x ) ) C_ No )
9	5 8	sylibr	|- ( x e. On -> ( ( _Made ` x ) \ ( _Old ` x ) ) e. ~P No )
10	1 9	fmpti	|- _New : On --> ~P No