Metamath Proof Explorer

Theorem funcoressn

Description: A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017)

Ref Expression
Assertion funcoressn 
|- ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( ( F o. G ) |` { X } ) )

Proof

Step Hyp Ref Expression
1 dmressnsn 
 |-  ( ( G ` X ) e. dom F -> dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } )
2 df-fn 
 |-  ( ( F |` { ( G ` X ) } ) Fn { ( G ` X ) } <-> ( Fun ( F |` { ( G ` X ) } ) /\ dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } ) )
3 2 simplbi2com 
 |-  ( dom ( F |` { ( G ` X ) } ) = { ( G ` X ) } -> ( Fun ( F |` { ( G ` X ) } ) -> ( F |` { ( G ` X ) } ) Fn { ( G ` X ) } ) )
4 1 3 syl 
 |-  ( ( G ` X ) e. dom F -> ( Fun ( F |` { ( G ` X ) } ) -> ( F |` { ( G ` X ) } ) Fn { ( G ` X ) } ) )
5 4 imp 
 |-  ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) -> ( F |` { ( G ` X ) } ) Fn { ( G ` X ) } )
6 5 adantr 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( F |` { ( G ` X ) } ) Fn { ( G ` X ) } )
7 fnsnfv 
 |-  ( ( G Fn A /\ X e. A ) -> { ( G ` X ) } = ( G " { X } ) )
8 7 adantl 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> { ( G ` X ) } = ( G " { X } ) )
9 df-ima 
 |-  ( G " { X } ) = ran ( G |` { X } )
10 8 9 eqtrdi 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> { ( G ` X ) } = ran ( G |` { X } ) )
11 10 reseq2d 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( F |` { ( G ` X ) } ) = ( F |` ran ( G |` { X } ) ) )
12 11 10 fneq12d 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( F |` { ( G ` X ) } ) Fn { ( G ` X ) } <-> ( F |` ran ( G |` { X } ) ) Fn ran ( G |` { X } ) ) )
13 6 12 mpbid 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( F |` ran ( G |` { X } ) ) Fn ran ( G |` { X } ) )
14 fnfun 
 |-  ( G Fn A -> Fun G )
15 funres 
 |-  ( Fun G -> Fun ( G |` { X } ) )
16 15 funfnd 
 |-  ( Fun G -> ( G |` { X } ) Fn dom ( G |` { X } ) )
17 14 16 syl 
 |-  ( G Fn A -> ( G |` { X } ) Fn dom ( G |` { X } ) )
18 17 adantr 
 |-  ( ( G Fn A /\ X e. A ) -> ( G |` { X } ) Fn dom ( G |` { X } ) )
19 18 adantl 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( G |` { X } ) Fn dom ( G |` { X } ) )
20 fnresfnco 
 |-  ( ( ( F |` ran ( G |` { X } ) ) Fn ran ( G |` { X } ) /\ ( G |` { X } ) Fn dom ( G |` { X } ) ) -> ( F o. ( G |` { X } ) ) Fn dom ( G |` { X } ) )
21 13 19 20 syl2anc 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( F o. ( G |` { X } ) ) Fn dom ( G |` { X } ) )
22 fnfun 
 |-  ( ( F o. ( G |` { X } ) ) Fn dom ( G |` { X } ) -> Fun ( F o. ( G |` { X } ) ) )
23 21 22 syl 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( F o. ( G |` { X } ) ) )
24 resco 
 |-  ( ( F o. G ) |` { X } ) = ( F o. ( G |` { X } ) )
25 24 funeqi 
 |-  ( Fun ( ( F o. G ) |` { X } ) <-> Fun ( F o. ( G |` { X } ) ) )
26 23 25 sylibr 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( ( F o. G ) |` { X } ) )