# Metamath Proof Explorer

## Theorem fununfun

Description: If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019)

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

### Proof

Step Hyp Ref Expression
1 funrel ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to \mathrm{Rel}\left({F}\cup {G}\right)$
2 relun ${⊢}\mathrm{Rel}\left({F}\cup {G}\right)↔\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)$
3 1 2 sylib ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to \left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)$
4 simpl ${⊢}\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\to \mathrm{Rel}{F}$
5 fununmo ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}$
6 5 alrimiv ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}$
7 4 6 anim12i ${⊢}\left(\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\wedge \mathrm{Fun}\left({F}\cup {G}\right)\right)\to \left(\mathrm{Rel}{F}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
8 dffun6 ${⊢}\mathrm{Fun}{F}↔\left(\mathrm{Rel}{F}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\right)$
9 7 8 sylibr ${⊢}\left(\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\wedge \mathrm{Fun}\left({F}\cup {G}\right)\right)\to \mathrm{Fun}{F}$
10 simpr ${⊢}\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\to \mathrm{Rel}{G}$
11 uncom ${⊢}{F}\cup {G}={G}\cup {F}$
12 11 funeqi ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)↔\mathrm{Fun}\left({G}\cup {F}\right)$
13 fununmo ${⊢}\mathrm{Fun}\left({G}\cup {F}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{G}{y}$
14 12 13 sylbi ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{G}{y}$
15 14 alrimiv ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{G}{y}$
16 10 15 anim12i ${⊢}\left(\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\wedge \mathrm{Fun}\left({F}\cup {G}\right)\right)\to \left(\mathrm{Rel}{G}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\right)$
17 dffun6 ${⊢}\mathrm{Fun}{G}↔\left(\mathrm{Rel}{G}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\right)$
18 16 17 sylibr ${⊢}\left(\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\wedge \mathrm{Fun}\left({F}\cup {G}\right)\right)\to \mathrm{Fun}{G}$
19 9 18 jca ${⊢}\left(\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)\wedge \mathrm{Fun}\left({F}\cup {G}\right)\right)\to \left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)$
20 3 19 mpancom ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to \left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)$