This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions fvco
Description: Value of a function composition. Similar to Exercise 5 of TakeutiZaring
p. 28. (Contributed by NM , 22-Apr-2006) (Proof shortened by Mario
Carneiro , 26-Dec-2014)
Ref
Expression
Assertion
fvco ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )
Proof
Step
Hyp
Ref
Expression
1
funfn ⊢ ( Fun 𝐺 ↔ 𝐺 Fn dom 𝐺 )
2
fvco2 ⊢ ( ( 𝐺 Fn dom 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )
3
1 2
sylanb ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )