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 dom F Fun F G X G Fn A X A Fun F G X

Proof

Step Hyp Ref Expression
1 dmressnsn G X 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 dom F Fun F G X F G X Fn G X
5 4 imp G X dom F Fun F G X F G X Fn G X
6 5 adantr G X dom F Fun F G X G Fn A X A F G X Fn G X
7 fnsnfv G Fn A X A G X = G X
8 7 adantl G X dom F Fun F G X G Fn A X A G X = G X
9 df-ima G X = ran G X
10 8 9 eqtrdi G X dom F Fun F G X G Fn A X A G X = ran G X
11 10 reseq2d G X dom F Fun F G X G Fn A X A F G X = F ran G X
12 11 10 fneq12d G X dom F Fun F G X G Fn A X A F G X Fn G X F ran G X Fn ran G X
13 6 12 mpbid G X dom F Fun F G X G Fn A X 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 A G X Fn dom G X
19 18 adantl G X dom F Fun F G X G Fn A X A G X Fn dom G X
20 fnresfnco F ran G X Fn ran G X G X Fn dom G X F G X Fn dom G X
21 13 19 20 syl2anc G X dom F Fun F G X G Fn A X A F G X Fn dom G X
22 fnfun F G X Fn dom G X Fun F G X
23 21 22 syl G X dom F Fun F G X G Fn A X A Fun F G X
24 resco F G X = F G X
25 24 funeqi Fun F G X Fun F G X
26 23 25 sylibr G X dom F Fun F G X G Fn A X A Fun F G X