Theorem staffn

Description: The functionalization is equal to the original function, if it is a function on the right base set. (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	staffn	$$⊢\underset{\dot{}}{\ast }FnB\to \underset{\dot{}}{\bullet }=\underset{\dot{}}{\ast }$$

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	1 2 3	staffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in B⟼\underset{\dot{}}{\ast }\left(x\right)\right)$$
5		dffn5	$$⊢\underset{\dot{}}{\ast }FnB\leftrightarrow \underset{\dot{}}{\ast }=\left(x\in B⟼\underset{\dot{}}{\ast }\left(x\right)\right)$$
6	5	biimpi	$$⊢\underset{\dot{}}{\ast }FnB\to \underset{\dot{}}{\ast }=\left(x\in B⟼\underset{\dot{}}{\ast }\left(x\right)\right)$$
7	4 6	eqtr4id	$$⊢\underset{\dot{}}{\ast }FnB\to \underset{\dot{}}{\bullet }=\underset{\dot{}}{\ast }$$