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	|- _M : On --> ~P No

Proof

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