Metamath Proof Explorer

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

Proof

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