Metamath Proof Explorer


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 |-