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 On M A = | s 𝒫 M A × 𝒫 M A

Proof

Step Hyp Ref Expression
1 df-made M = recs x V | s 𝒫 ran x × 𝒫 ran x
2 1 tfr2 A On M A = x V | s 𝒫 ran x × 𝒫 ran x M A
3 eqid x V | s 𝒫 ran x × 𝒫 ran x = x V | s 𝒫 ran x × 𝒫 ran x
4 rneq x = M A ran x = ran M A
5 df-ima M A = ran M A
6 4 5 syl6eqr x = M A ran x = M A
7 6 unieqd x = M A ran x = M A
8 7 pweqd x = M A 𝒫 ran x = 𝒫 M A
9 8 sqxpeqd x = M A 𝒫 ran x × 𝒫 ran x = 𝒫 M A × 𝒫 M A
10 9 imaeq2d x = M A | s 𝒫 ran x × 𝒫 ran x = | s 𝒫 M A × 𝒫 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 On M A V
15 13 14 mpan A On M A V
16 scutf | s : s No
17 ffun | s : s No Fun | s
18 16 17 ax-mp Fun | s
19 funimaexg Fun M A On M A V
20 13 19 mpan A On M A V
21 uniexg M A V M A V
22 pwexg M A V 𝒫 M A V
23 20 21 22 3syl A On 𝒫 M A V
24 23 23 xpexd A On 𝒫 M A × 𝒫 M A V
25 funimaexg Fun | s 𝒫 M A × 𝒫 M A V | s 𝒫 M A × 𝒫 M A V
26 18 24 25 sylancr A On | s 𝒫 M A × 𝒫 M A V
27 3 10 15 26 fvmptd3 A On x V | s 𝒫 ran x × 𝒫 ran x M A = | s 𝒫 M A × 𝒫 M A
28 2 27 eqtrd A On M A = | s 𝒫 M A × 𝒫 M A