# Metamath Proof Explorer

## Theorem fnco

Description: Composition of two functions. (Contributed by NM, 22-May-2006)

Ref Expression
Assertion fnco ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \left({F}\circ {G}\right)Fn{B}$

### Proof

Step Hyp Ref Expression
1 fnfun ${⊢}{F}Fn{A}\to \mathrm{Fun}{F}$
2 fnfun ${⊢}{G}Fn{B}\to \mathrm{Fun}{G}$
3 funco ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \mathrm{Fun}\left({F}\circ {G}\right)$
4 1 2 3 syl2an ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \mathrm{Fun}\left({F}\circ {G}\right)$
5 4 3adant3 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \mathrm{Fun}\left({F}\circ {G}\right)$
6 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
7 6 sseq2d ${⊢}{F}Fn{A}\to \left(\mathrm{ran}{G}\subseteq \mathrm{dom}{F}↔\mathrm{ran}{G}\subseteq {A}\right)$
8 7 biimpar ${⊢}\left({F}Fn{A}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \mathrm{ran}{G}\subseteq \mathrm{dom}{F}$
9 dmcosseq ${⊢}\mathrm{ran}{G}\subseteq \mathrm{dom}{F}\to \mathrm{dom}\left({F}\circ {G}\right)=\mathrm{dom}{G}$
10 8 9 syl ${⊢}\left({F}Fn{A}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \mathrm{dom}\left({F}\circ {G}\right)=\mathrm{dom}{G}$
11 10 3adant2 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \mathrm{dom}\left({F}\circ {G}\right)=\mathrm{dom}{G}$
12 fndm ${⊢}{G}Fn{B}\to \mathrm{dom}{G}={B}$
13 12 3ad2ant2 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \mathrm{dom}{G}={B}$
14 11 13 eqtrd ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \mathrm{dom}\left({F}\circ {G}\right)={B}$
15 df-fn ${⊢}\left({F}\circ {G}\right)Fn{B}↔\left(\mathrm{Fun}\left({F}\circ {G}\right)\wedge \mathrm{dom}\left({F}\circ {G}\right)={B}\right)$
16 5 14 15 sylanbrc ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {A}\right)\to \left({F}\circ {G}\right)Fn{B}$