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

Metamath Proof Explorer

Theorem fncofn

Description: Composition of a function with domain and a function as a function with domain. Generalization of fnco . (Contributed by AV, 17-Sep-2024)

Ref Expression
Assertion fncofn 
|- ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( F Fn A -> Fun F )
2 funco 
 |-  ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
3 1 2 sylan 
 |-  ( ( F Fn A /\ Fun G ) -> Fun ( F o. G ) )
4 3 funfnd 
 |-  ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn dom ( F o. G ) )
5 fndm 
 |-  ( F Fn A -> dom F = A )
6 5 adantr 
 |-  ( ( F Fn A /\ Fun G ) -> dom F = A )
7 6 eqcomd 
 |-  ( ( F Fn A /\ Fun G ) -> A = dom F )
8 7 imaeq2d 
 |-  ( ( F Fn A /\ Fun G ) -> ( `' G " A ) = ( `' G " dom F ) )
9 dmco 
 |-  dom ( F o. G ) = ( `' G " dom F )
10 8 9 eqtr4di 
 |-  ( ( F Fn A /\ Fun G ) -> ( `' G " A ) = dom ( F o. G ) )
11 10 fneq2d 
 |-  ( ( F Fn A /\ Fun G ) -> ( ( F o. G ) Fn ( `' G " A ) <-> ( F o. G ) Fn dom ( F o. G ) ) )
12 4 11 mpbird 
 |-  ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )