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	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	staffval.f	$$⊢\underset{\dot{}}{\bullet }={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
Assertion	staffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in B⟼\underset{\dot{}}{\ast }\left(x\right)\right)$$

Proof

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