# Metamath Proof Explorer

## Theorem staffval

Description: The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses staffval.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
staffval.i
staffval.f
Assertion staffval

### Proof

Step Hyp Ref Expression
1 staffval.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 staffval.i
3 staffval.f
4 fveq2 ${⊢}{f}={R}\to {\mathrm{Base}}_{{f}}={\mathrm{Base}}_{{R}}$
5 4 1 syl6eqr ${⊢}{f}={R}\to {\mathrm{Base}}_{{f}}={B}$
6 fveq2 ${⊢}{f}={R}\to {*}_{{f}}={*}_{{R}}$
7 6 2 syl6eqr
8 7 fveq1d
9 5 8 mpteq12dv
10 df-staf ${⊢}{\ast }_{\mathrm{𝑟𝑓}}=\left({f}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{f}}⟼{{x}}^{{*}_{{f}}}\right)\right)$
11 eqid
12 fvrn0
13 12 a1i
14 11 13 fmpti
15 1 fvexi ${⊢}{B}\in \mathrm{V}$
16 2 fvexi
17 16 rnex
18 p0ex ${⊢}\left\{\varnothing \right\}\in \mathrm{V}$
19 17 18 unex
20 fex2
21 14 15 19 20 mp3an
22 9 10 21 fvmpt
23 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)=\varnothing$
24 mpt0
25 23 24 syl6eqr
26 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{Base}}_{{R}}=\varnothing$
27 1 26 syl5eq ${⊢}¬{R}\in \mathrm{V}\to {B}=\varnothing$
28 27 mpteq1d
29 25 28 eqtr4d
30 22 29 pm2.61i
31 3 30 eqtri