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	Could not format assertion : No typesetting found for |- _New : On --> ~P No with typecode |-

Proof

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