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 ⊢ 𝐵 = ( 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 𝐵 → ∙ = ∗ )