Theorem madef

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

	Ref	Expression
Assertion	madef	Could not format assertion : No typesetting found for |- _Made : On --> ~P No with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-made	Could not format _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) : No typesetting found for |- _Made = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) with typecode |-
2	1	tfr1	Could not format _Made Fn On : No typesetting found for |- _Made Fn On with typecode |-
3		madeval2	Could not format ( x e. On -> ( _Made ` x ) = { y e. No | E. z e. ~P U. ( _Made " x ) E. w e. ~P U. ( _Made " x ) ( z < ( _Made ` x ) = { y e. No | E. z e. ~P U. ( _Made " x ) E. w e. ~P U. ( _Made " x ) ( z <
4		ssrab2	Could not format { y e. No | E. z e. ~P U. ( _Made " x ) E. w e. ~P U. ( _Made " x ) ( z <
5	3 4	eqsstrdi	Could not format ( x e. On -> ( _Made ` x ) C_ No ) : No typesetting found for |- ( x e. On -> ( _Made ` x ) C_ No ) with typecode |-
6		sseq1	Could not format ( y = ( _Made ` x ) -> ( y C_ No <-> ( _Made ` x ) C_ No ) ) : No typesetting found for |- ( y = ( _Made ` x ) -> ( y C_ No <-> ( _Made ` x ) C_ No ) ) with typecode |-
7	5 6	syl5ibrcom	Could not format ( x e. On -> ( y = ( _Made ` x ) -> y C_ No ) ) : No typesetting found for |- ( x e. On -> ( y = ( _Made ` x ) -> y C_ No ) ) with typecode |-
8	7	rexlimiv	Could not format ( E. x e. On y = ( _Made ` x ) -> y C_ No ) : No typesetting found for |- ( E. x e. On y = ( _Made ` x ) -> y C_ No ) with typecode |-
9		vex	$$⊢y\in \mathrm{V}$$
10		eqeq1	Could not format ( z = y -> ( z = ( _Made ` x ) <-> y = ( _Made ` x ) ) ) : No typesetting found for |- ( z = y -> ( z = ( _Made ` x ) <-> y = ( _Made ` x ) ) ) with typecode |-
11	10	rexbidv	Could not format ( z = y -> ( E. x e. On z = ( _Made ` x ) <-> E. x e. On y = ( _Made ` x ) ) ) : No typesetting found for |- ( z = y -> ( E. x e. On z = ( _Made ` x ) <-> E. x e. On y = ( _Made ` x ) ) ) with typecode |-
12		fnrnfv	Could not format ( _Made Fn On -> ran _Made = { z | E. x e. On z = ( _Made ` x ) } ) : No typesetting found for |- ( _Made Fn On -> ran _Made = { z | E. x e. On z = ( _Made ` x ) } ) with typecode |-
13	2 12	ax-mp	Could not format ran _Made = { z | E. x e. On z = ( _Made ` x ) } : No typesetting found for |- ran _Made = { z | E. x e. On z = ( _Made ` x ) } with typecode |-
14	9 11 13	elab2	Could not format ( y e. ran _Made <-> E. x e. On y = ( _Made ` x ) ) : No typesetting found for |- ( y e. ran _Made <-> E. x e. On y = ( _Made ` x ) ) with typecode |-
15		velpw	$$⊢y\in 𝒫\mathrm{No}\leftrightarrow y\subseteq \mathrm{No}$$
16	8 14 15	3imtr4i	Could not format ( y e. ran _Made -> y e. ~P No ) : No typesetting found for |- ( y e. ran _Made -> y e. ~P No ) with typecode |-
17	16	ssriv	Could not format ran _Made C_ ~P No : No typesetting found for |- ran _Made C_ ~P No with typecode |-
18		df-f	Could not format ( _Made : On --> ~P No <-> ( _Made Fn On /\ ran _Made C_ ~P No ) ) : No typesetting found for |- ( _Made : On --> ~P No <-> ( _Made Fn On /\ ran _Made C_ ~P No ) ) with typecode |-
19	2 17 18	mpbir2an	Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-