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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	staffval.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
	staffval.f	⊢ ∙ = ( *rf ‘ 𝑅 )
Assertion	staffn	⊢ ( ∗ Fn 𝐵 → ∙ = ∗ )

Proof

Step	Hyp	Ref	Expression
1		staffval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		staffval.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
3		staffval.f	⊢ ∙ = ( *rf ‘ 𝑅 )
4	1 2 3	staffval	⊢ ∙ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) )
5		dffn5	⊢ ( ∗ Fn 𝐵 ↔ ∗ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) )
6	5	biimpi	⊢ ( ∗ Fn 𝐵 → ∗ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) )
7	4 6	eqtr4id	⊢ ( ∗ Fn 𝐵 → ∙ = ∗ )