# Metamath Proof Explorer

## Theorem funco

Description: The composition of two functions is a function. Exercise 29 of TakeutiZaring p. 25. (Contributed by NM, 26-Jan-1997) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion funco ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \mathrm{Fun}\left({F}\circ {G}\right)$

### Proof

Step Hyp Ref Expression
1 funmo ${⊢}\mathrm{Fun}{G}\to {\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{x}{G}{z}$
2 funmo ${⊢}\mathrm{Fun}{F}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{z}{F}{y}$
3 2 alrimiv ${⊢}\mathrm{Fun}{F}\to \forall {z}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{z}{F}{y}$
4 moexexvw ${⊢}\left({\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{x}{G}{z}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{z}{F}{y}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)$
5 1 3 4 syl2anr ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)$
6 5 alrimiv ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)$
7 funopab ${⊢}\mathrm{Fun}\left\{⟨{x},{y}⟩|\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)$
8 6 7 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \mathrm{Fun}\left\{⟨{x},{y}⟩|\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)\right\}$
9 df-co ${⊢}{F}\circ {G}=\left\{⟨{x},{y}⟩|\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)\right\}$
10 9 funeqi ${⊢}\mathrm{Fun}\left({F}\circ {G}\right)↔\mathrm{Fun}\left\{⟨{x},{y}⟩|\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\wedge {z}{F}{y}\right)\right\}$
11 8 10 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \mathrm{Fun}\left({F}\circ {G}\right)$