Metamath Proof Explorer

Theorem oldf

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

Ref Expression
Assertion oldf 
|- _Old : On --> ~P No

Proof

Step Hyp Ref Expression
1 df-old 
 |-  _Old = ( x e. On |-> U. ( _Made " x ) )
2 imassrn 
 |-  ( _Made " x ) C_ ran _Made
3 madef 
 |-  _Made : On --> ~P No
4 frn 
 |-  ( _Made : On --> ~P No -> ran _Made C_ ~P No )
5 3 4 ax-mp 
 |-  ran _Made C_ ~P No
6 2 5 sstri 
 |-  ( _Made " x ) C_ ~P No
7 6 sseli 
 |-  ( y e. ( _Made " x ) -> y e. ~P No )
8 7 elpwid 
 |-  ( y e. ( _Made " x ) -> y C_ No )
9 8 rgen 
 |-  A. y e. ( _Made " x ) y C_ No
10 9 a1i 
 |-  ( x e. On -> A. y e. ( _Made " x ) y C_ No )
11 ffun 
 |-  ( _Made : On --> ~P No -> Fun _Made )
12 3 11 ax-mp 
 |-  Fun _Made
13 vex 
 |-  x e. _V
14 13 funimaex 
 |-  ( Fun _Made -> ( _Made " x ) e. _V )
15 12 14 ax-mp 
 |-  ( _Made " x ) e. _V
16 15 uniex 
 |-  U. ( _Made " x ) e. _V
17 16 elpw 
 |-  ( U. ( _Made " x ) e. ~P No <-> U. ( _Made " x ) C_ No )
18 unissb 
 |-  ( U. ( _Made " x ) C_ No <-> A. y e. ( _Made " x ) y C_ No )
19 17 18 bitri 
 |-  ( U. ( _Made " x ) e. ~P No <-> A. y e. ( _Made " x ) y C_ No )
20 10 19 sylibr 
 |-  ( x e. On -> U. ( _Made " x ) e. ~P No )
21 1 20 fmpti 
 |-  _Old : On --> ~P No