Metamath Proof Explorer

Theorem fvco4i

Description: Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Hypotheses fvco4i.a 
|- (/) = ( F ` (/) )
fvco4i.b 
|- Fun G
Assertion fvco4i 
|- ( ( F o. G ) ` X ) = ( F ` ( G ` X ) )

Proof

Step Hyp Ref Expression
1 fvco4i.a 
 |-  (/) = ( F ` (/) )
2 fvco4i.b 
 |-  Fun G
3 funfn 
 |-  ( Fun G <-> G Fn dom G )
4 2 3 mpbi 
 |-  G Fn dom G
5 fvco2 
 |-  ( ( G Fn dom G /\ X e. dom G ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
6 4 5 mpan 
 |-  ( X e. dom G -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
7 dmcoss 
 |-  dom ( F o. G ) C_ dom G
8 7 sseli 
 |-  ( X e. dom ( F o. G ) -> X e. dom G )
9 ndmfv 
 |-  ( -. X e. dom ( F o. G ) -> ( ( F o. G ) ` X ) = (/) )
10 8 9 nsyl5 
 |-  ( -. X e. dom G -> ( ( F o. G ) ` X ) = (/) )
11 ndmfv 
 |-  ( -. X e. dom G -> ( G ` X ) = (/) )
12 11 fveq2d 
 |-  ( -. X e. dom G -> ( F ` ( G ` X ) ) = ( F ` (/) ) )
13 1 10 12 3eqtr4a 
 |-  ( -. X e. dom G -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
14 6 13 pm2.61i 
 |-  ( ( F o. G ) ` X ) = ( F ` ( G ` X ) )