# Metamath Proof Explorer

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

Ref Expression
Assertion madeval ${⊢}{A}\in \mathrm{On}\to M\left({A}\right)={|}_{s}\left[𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\right]$

### Proof

Step Hyp Ref Expression
1 df-made ${⊢}M=\mathrm{recs}\left(\left({x}\in \mathrm{V}⟼{|}_{s}\left[𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}\right]\right)\right)$
2 1 tfr2 ${⊢}{A}\in \mathrm{On}\to M\left({A}\right)=\left({x}\in \mathrm{V}⟼{|}_{s}\left[𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}\right]\right)\left({M↾}_{{A}}\right)$
3 eqid ${⊢}\left({x}\in \mathrm{V}⟼{|}_{s}\left[𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}\right]\right)=\left({x}\in \mathrm{V}⟼{|}_{s}\left[𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}\right]\right)$
4 rneq ${⊢}{x}={M↾}_{{A}}\to \mathrm{ran}{x}=\mathrm{ran}\left({M↾}_{{A}}\right)$
5 df-ima ${⊢}M\left[{A}\right]=\mathrm{ran}\left({M↾}_{{A}}\right)$
6 4 5 syl6eqr ${⊢}{x}={M↾}_{{A}}\to \mathrm{ran}{x}=M\left[{A}\right]$
7 6 unieqd ${⊢}{x}={M↾}_{{A}}\to \bigcup \mathrm{ran}{x}=\bigcup M\left[{A}\right]$
8 7 pweqd ${⊢}{x}={M↾}_{{A}}\to 𝒫\bigcup \mathrm{ran}{x}=𝒫\bigcup M\left[{A}\right]$
9 8 sqxpeqd ${⊢}{x}={M↾}_{{A}}\to 𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}=𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]$
10 9 imaeq2d ${⊢}{x}={M↾}_{{A}}\to {|}_{s}\left[𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}\right]={|}_{s}\left[𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\right]$
11 1 tfr1 ${⊢}MFn\mathrm{On}$
12 fnfun ${⊢}MFn\mathrm{On}\to \mathrm{Fun}M$
13 11 12 ax-mp ${⊢}\mathrm{Fun}M$
14 resfunexg ${⊢}\left(\mathrm{Fun}M\wedge {A}\in \mathrm{On}\right)\to {M↾}_{{A}}\in \mathrm{V}$
15 13 14 mpan ${⊢}{A}\in \mathrm{On}\to {M↾}_{{A}}\in \mathrm{V}$
16 scutf ${⊢}{|}_{s}:{\ll }_{s}⟶\mathrm{No}$
17 ffun ${⊢}{|}_{s}:{\ll }_{s}⟶\mathrm{No}\to \mathrm{Fun}{|}_{s}$
18 16 17 ax-mp ${⊢}\mathrm{Fun}{|}_{s}$
19 funimaexg ${⊢}\left(\mathrm{Fun}M\wedge {A}\in \mathrm{On}\right)\to M\left[{A}\right]\in \mathrm{V}$
20 13 19 mpan ${⊢}{A}\in \mathrm{On}\to M\left[{A}\right]\in \mathrm{V}$
21 uniexg ${⊢}M\left[{A}\right]\in \mathrm{V}\to \bigcup M\left[{A}\right]\in \mathrm{V}$
22 pwexg ${⊢}\bigcup M\left[{A}\right]\in \mathrm{V}\to 𝒫\bigcup M\left[{A}\right]\in \mathrm{V}$
23 20 21 22 3syl ${⊢}{A}\in \mathrm{On}\to 𝒫\bigcup M\left[{A}\right]\in \mathrm{V}$
24 23 23 xpexd ${⊢}{A}\in \mathrm{On}\to 𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\in \mathrm{V}$
25 funimaexg ${⊢}\left(\mathrm{Fun}{|}_{s}\wedge 𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\in \mathrm{V}\right)\to {|}_{s}\left[𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\right]\in \mathrm{V}$
26 18 24 25 sylancr ${⊢}{A}\in \mathrm{On}\to {|}_{s}\left[𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\right]\in \mathrm{V}$
27 3 10 15 26 fvmptd3 ${⊢}{A}\in \mathrm{On}\to \left({x}\in \mathrm{V}⟼{|}_{s}\left[𝒫\bigcup \mathrm{ran}{x}×𝒫\bigcup \mathrm{ran}{x}\right]\right)\left({M↾}_{{A}}\right)={|}_{s}\left[𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\right]$
28 2 27 eqtrd ${⊢}{A}\in \mathrm{On}\to M\left({A}\right)={|}_{s}\left[𝒫\bigcup M\left[{A}\right]×𝒫\bigcup M\left[{A}\right]\right]$