This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{R}$
		staffval.i	$⊢ \underset{˙}{} = _{R}$
		staffval.f	$⊢ \underset{˙}{∙} = *_{𝑟𝑓} (R)$
	Assertion	staffn	$⊢ \underset{˙}{} Fn B \to \underset{˙}{∙} = \underset{˙}{}$

Proof

Step	Hyp	Ref	Expression
1		staffval.b	$⊢ B = {Base}_{R}$
2		staffval.i	$⊢ \underset{˙}{} = _{R}$
3		staffval.f	$⊢ \underset{˙}{∙} = *_{𝑟𝑓} (R)$
4	1 2 3	staffval	$⊢ \underset{˙}{∙} = (x \in B ⟼ \underset{˙}{*} (x))$
5		dffn5	$⊢ \underset{˙}{} Fn B \leftrightarrow \underset{˙}{} = (x \in B ⟼ \underset{˙}{*} (x))$
6	5	biimpi	$⊢ \underset{˙}{} Fn B \to \underset{˙}{} = (x \in B ⟼ \underset{˙}{*} (x))$
7	4 6	eqtr4id	$⊢ \underset{˙}{} Fn B \to \underset{˙}{∙} = \underset{˙}{}$