# Metamath Proof Explorer

## Theorem funun

Description: The union of functions with disjoint domains is a function. Theorem 4.6 of Monk1 p. 43. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion funun ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \mathrm{Fun}\left({F}\cup {G}\right)$

### Proof

Step Hyp Ref Expression
1 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
2 funrel ${⊢}\mathrm{Fun}{G}\to \mathrm{Rel}{G}$
3 1 2 anim12i ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)$
4 relun ${⊢}\mathrm{Rel}\left({F}\cup {G}\right)↔\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}{G}\right)$
5 3 4 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \mathrm{Rel}\left({F}\cup {G}\right)$
6 5 adantr ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \mathrm{Rel}\left({F}\cup {G}\right)$
7 elun ${⊢}⟨{x},{y}⟩\in \left({F}\cup {G}\right)↔\left(⟨{x},{y}⟩\in {F}\vee ⟨{x},{y}⟩\in {G}\right)$
8 elun ${⊢}⟨{x},{z}⟩\in \left({F}\cup {G}\right)↔\left(⟨{x},{z}⟩\in {F}\vee ⟨{x},{z}⟩\in {G}\right)$
9 7 8 anbi12i ${⊢}\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)↔\left(\left(⟨{x},{y}⟩\in {F}\vee ⟨{x},{y}⟩\in {G}\right)\wedge \left(⟨{x},{z}⟩\in {F}\vee ⟨{x},{z}⟩\in {G}\right)\right)$
10 anddi ${⊢}\left(\left(⟨{x},{y}⟩\in {F}\vee ⟨{x},{y}⟩\in {G}\right)\wedge \left(⟨{x},{z}⟩\in {F}\vee ⟨{x},{z}⟩\in {G}\right)\right)↔\left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\vee \left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)$
11 9 10 bitri ${⊢}\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)↔\left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\vee \left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)$
12 disj1 ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\to ¬{x}\in \mathrm{dom}{G}\right)$
13 12 biimpi ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\to ¬{x}\in \mathrm{dom}{G}\right)$
14 13 19.21bi ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to \left({x}\in \mathrm{dom}{F}\to ¬{x}\in \mathrm{dom}{G}\right)$
15 imnan ${⊢}\left({x}\in \mathrm{dom}{F}\to ¬{x}\in \mathrm{dom}{G}\right)↔¬\left({x}\in \mathrm{dom}{F}\wedge {x}\in \mathrm{dom}{G}\right)$
16 14 15 sylib ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to ¬\left({x}\in \mathrm{dom}{F}\wedge {x}\in \mathrm{dom}{G}\right)$
17 vex ${⊢}{x}\in \mathrm{V}$
18 vex ${⊢}{y}\in \mathrm{V}$
19 17 18 opeldm ${⊢}⟨{x},{y}⟩\in {F}\to {x}\in \mathrm{dom}{F}$
20 vex ${⊢}{z}\in \mathrm{V}$
21 17 20 opeldm ${⊢}⟨{x},{z}⟩\in {G}\to {x}\in \mathrm{dom}{G}$
22 19 21 anim12i ${⊢}\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left({x}\in \mathrm{dom}{F}\wedge {x}\in \mathrm{dom}{G}\right)$
23 16 22 nsyl ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to ¬\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)$
24 orel2 ${⊢}¬\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\right)$
25 23 24 syl ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to \left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\right)$
26 14 con2d ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to \left({x}\in \mathrm{dom}{G}\to ¬{x}\in \mathrm{dom}{F}\right)$
27 imnan ${⊢}\left({x}\in \mathrm{dom}{G}\to ¬{x}\in \mathrm{dom}{F}\right)↔¬\left({x}\in \mathrm{dom}{G}\wedge {x}\in \mathrm{dom}{F}\right)$
28 26 27 sylib ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to ¬\left({x}\in \mathrm{dom}{G}\wedge {x}\in \mathrm{dom}{F}\right)$
29 17 18 opeldm ${⊢}⟨{x},{y}⟩\in {G}\to {x}\in \mathrm{dom}{G}$
30 17 20 opeldm ${⊢}⟨{x},{z}⟩\in {F}\to {x}\in \mathrm{dom}{F}$
31 29 30 anim12i ${⊢}\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\to \left({x}\in \mathrm{dom}{G}\wedge {x}\in \mathrm{dom}{F}\right)$
32 28 31 nsyl ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to ¬\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)$
33 orel1 ${⊢}¬\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\to \left(\left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)$
34 32 33 syl ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to \left(\left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)$
35 25 34 orim12d ${⊢}\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \to \left(\left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\vee \left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)$
36 35 adantl ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left(\left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\vee \left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)$
37 11 36 syl5bi ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left(\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\right)$
38 dffun4 ${⊢}\mathrm{Fun}{F}↔\left(\mathrm{Rel}{F}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)\right)$
39 38 simprbi ${⊢}\mathrm{Fun}{F}\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)$
40 39 19.21bi ${⊢}\mathrm{Fun}{F}\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)$
41 40 19.21bbi ${⊢}\mathrm{Fun}{F}\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)$
42 dffun4 ${⊢}\mathrm{Fun}{G}↔\left(\mathrm{Rel}{G}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\to {y}={z}\right)\right)$
43 42 simprbi ${⊢}\mathrm{Fun}{G}\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\to {y}={z}\right)$
44 43 19.21bi ${⊢}\mathrm{Fun}{G}\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\to {y}={z}\right)$
45 44 19.21bbi ${⊢}\mathrm{Fun}{G}\to \left(\left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\to {y}={z}\right)$
46 41 45 jaao ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to {y}={z}\right)$
47 46 adantr ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left(\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\vee \left(⟨{x},{y}⟩\in {G}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to {y}={z}\right)$
48 37 47 syld ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left(\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)\to {y}={z}\right)$
49 48 alrimiv ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)\to {y}={z}\right)$
50 49 alrimivv ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)\to {y}={z}\right)$
51 dffun4 ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)↔\left(\mathrm{Rel}\left({F}\cup {G}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in \left({F}\cup {G}\right)\wedge ⟨{x},{z}⟩\in \left({F}\cup {G}\right)\right)\to {y}={z}\right)\right)$
52 6 50 51 sylanbrc ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \mathrm{Fun}\left({F}\cup {G}\right)$