Metamath Proof Explorer

Theorem oldval

Description: The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024)

Ref Expression
Assertion oldval 
|- ( A e. On -> ( _Old ` A ) = U. ( _M " A ) )

Proof

Step Hyp Ref Expression
1 df-made 
 |-  _M = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) )
2 recsfnon 
 |-  recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) Fn On
3 fnfun 
 |-  ( recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) Fn On -> Fun recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) )
4 2 3 ax-mp 
 |-  Fun recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) )
5 funeq 
 |-  ( _M = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) -> ( Fun _M <-> Fun recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) ) )
6 4 5 mpbiri 
 |-  ( _M = recs ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ) -> Fun _M )
7 1 6 ax-mp 
 |-  Fun _M
8 funimaexg 
 |-  ( ( Fun _M /\ A e. On ) -> ( _M " A ) e. _V )
9 7 8 mpan 
 |-  ( A e. On -> ( _M " A ) e. _V )
10 9 uniexd 
 |-  ( A e. On -> U. ( _M " A ) e. _V )
11 imaeq2 
 |-  ( x = A -> ( _M " x ) = ( _M " A ) )
12 11 unieqd 
 |-  ( x = A -> U. ( _M " x ) = U. ( _M " A ) )
13 df-old 
 |-  _Old = ( x e. On |-> U. ( _M " x ) )
14 12 13 fvmptg 
 |-  ( ( A e. On /\ U. ( _M " A ) e. _V ) -> ( _Old ` A ) = U. ( _M " A ) )
15 10 14 mpdan 
 |-  ( A e. On -> ( _Old ` A ) = U. ( _M " A ) )