Metamath Proof Explorer

Theorem madeval

Description: The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)

Ref Expression
Assertion madeval 
|- ( A e. On -> ( _M ` A ) = ( |s " ( ~P U. ( _M " A ) X. ~P 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 1 tfr2 
 |-  ( A e. On -> ( _M ` A ) = ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ` ( _M |` A ) ) )
3 eqid 
 |-  ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) = ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) )
4 rneq 
 |-  ( x = ( _M |` A ) -> ran x = ran ( _M |` A ) )
5 df-ima 
 |-  ( _M " A ) = ran ( _M |` A )
6 4 5 eqtr4di 
 |-  ( x = ( _M |` A ) -> ran x = ( _M " A ) )
7 6 unieqd 
 |-  ( x = ( _M |` A ) -> U. ran x = U. ( _M " A ) )
8 7 pweqd 
 |-  ( x = ( _M |` A ) -> ~P U. ran x = ~P U. ( _M " A ) )
9 8 sqxpeqd 
 |-  ( x = ( _M |` A ) -> ( ~P U. ran x X. ~P U. ran x ) = ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) )
10 9 imaeq2d 
 |-  ( x = ( _M |` A ) -> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) = ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) )
11 1 tfr1 
 |-  _M Fn On
12 fnfun 
 |-  ( _M Fn On -> Fun _M )
13 11 12 ax-mp 
 |-  Fun _M
14 resfunexg 
 |-  ( ( Fun _M /\ A e. On ) -> ( _M |` A ) e. _V )
15 13 14 mpan 
 |-  ( A e. On -> ( _M |` A ) e. _V )
16 scutf 
 |-  |s : < No
17 ffun 
 |-  ( |s : < No -> Fun |s )
18 16 17 ax-mp 
 |-  Fun |s
19 funimaexg 
 |-  ( ( Fun _M /\ A e. On ) -> ( _M " A ) e. _V )
20 13 19 mpan 
 |-  ( A e. On -> ( _M " A ) e. _V )
21 uniexg 
 |-  ( ( _M " A ) e. _V -> U. ( _M " A ) e. _V )
22 pwexg 
 |-  ( U. ( _M " A ) e. _V -> ~P U. ( _M " A ) e. _V )
23 20 21 22 3syl 
 |-  ( A e. On -> ~P U. ( _M " A ) e. _V )
24 23 23 xpexd 
 |-  ( A e. On -> ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) e. _V )
25 funimaexg 
 |-  ( ( Fun |s /\ ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) e. _V ) -> ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) e. _V )
26 18 24 25 sylancr 
 |-  ( A e. On -> ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) e. _V )
27 3 10 15 26 fvmptd3 
 |-  ( A e. On -> ( ( x e. _V |-> ( |s " ( ~P U. ran x X. ~P U. ran x ) ) ) ` ( _M |` A ) ) = ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) )
28 2 27 eqtrd 
 |-  ( A e. On -> ( _M ` A ) = ( |s " ( ~P U. ( _M " A ) X. ~P U. ( _M " A ) ) ) )