# 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
`|- ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )`

### Proof

Step Hyp Ref Expression
1 funrel
` |-  ( Fun F -> Rel F )`
2 funrel
` |-  ( Fun G -> Rel G )`
3 1 2 anim12i
` |-  ( ( Fun F /\ Fun G ) -> ( Rel F /\ Rel G ) )`
4 relun
` |-  ( Rel ( F u. G ) <-> ( Rel F /\ Rel G ) )`
5 3 4 sylibr
` |-  ( ( Fun F /\ Fun G ) -> Rel ( F u. G ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Rel ( F u. G ) )`
7 elun
` |-  ( <. x , y >. e. ( F u. G ) <-> ( <. x , y >. e. F \/ <. x , y >. e. G ) )`
8 elun
` |-  ( <. x , z >. e. ( F u. G ) <-> ( <. x , z >. e. F \/ <. x , z >. e. G ) )`
9 7 8 anbi12i
` |-  ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) <-> ( ( <. x , y >. e. F \/ <. x , y >. e. G ) /\ ( <. x , z >. e. F \/ <. x , z >. e. G ) ) )`
10 anddi
` |-  ( ( ( <. x , y >. e. F \/ <. x , y >. e. G ) /\ ( <. x , z >. e. F \/ <. x , z >. e. G ) ) <-> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) \/ ( ( <. x , y >. e. G /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) )`
11 9 10 bitri
` |-  ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) <-> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) \/ ( ( <. x , y >. e. G /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) )`
12 disj1
` |-  ( ( dom F i^i dom G ) = (/) <-> A. x ( x e. dom F -> -. x e. dom G ) )`
13 12 biimpi
` |-  ( ( dom F i^i dom G ) = (/) -> A. x ( x e. dom F -> -. x e. dom G ) )`
14 13 19.21bi
` |-  ( ( dom F i^i dom G ) = (/) -> ( x e. dom F -> -. x e. dom G ) )`
15 imnan
` |-  ( ( x e. dom F -> -. x e. dom G ) <-> -. ( x e. dom F /\ x e. dom G ) )`
16 14 15 sylib
` |-  ( ( dom F i^i dom G ) = (/) -> -. ( x e. dom F /\ x e. dom G ) )`
17 vex
` |-  x e. _V`
18 vex
` |-  y e. _V`
19 17 18 opeldm
` |-  ( <. x , y >. e. F -> x e. dom F )`
20 vex
` |-  z e. _V`
21 17 20 opeldm
` |-  ( <. x , z >. e. G -> x e. dom G )`
22 19 21 anim12i
` |-  ( ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( x e. dom F /\ x e. dom G ) )`
23 16 22 nsyl
` |-  ( ( dom F i^i dom G ) = (/) -> -. ( <. x , y >. e. F /\ <. x , z >. e. G ) )`
24 orel2
` |-  ( -. ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) -> ( <. x , y >. e. F /\ <. x , z >. e. F ) ) )`
25 23 24 syl
` |-  ( ( dom F i^i dom G ) = (/) -> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) -> ( <. x , y >. e. F /\ <. x , z >. e. F ) ) )`
26 14 con2d
` |-  ( ( dom F i^i dom G ) = (/) -> ( x e. dom G -> -. x e. dom F ) )`
27 imnan
` |-  ( ( x e. dom G -> -. x e. dom F ) <-> -. ( x e. dom G /\ x e. dom F ) )`
28 26 27 sylib
` |-  ( ( dom F i^i dom G ) = (/) -> -. ( x e. dom G /\ x e. dom F ) )`
29 17 18 opeldm
` |-  ( <. x , y >. e. G -> x e. dom G )`
30 17 20 opeldm
` |-  ( <. x , z >. e. F -> x e. dom F )`
31 29 30 anim12i
` |-  ( ( <. x , y >. e. G /\ <. x , z >. e. F ) -> ( x e. dom G /\ x e. dom F ) )`
32 28 31 nsyl
` |-  ( ( dom F i^i dom G ) = (/) -> -. ( <. x , y >. e. G /\ <. x , z >. e. F ) )`
33 orel1
` |-  ( -. ( <. x , y >. e. G /\ <. x , z >. e. F ) -> ( ( ( <. x , y >. e. G /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) -> ( <. x , y >. e. G /\ <. x , z >. e. G ) ) )`
34 32 33 syl
` |-  ( ( dom F i^i dom G ) = (/) -> ( ( ( <. x , y >. e. G /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) -> ( <. x , y >. e. G /\ <. x , z >. e. G ) ) )`
35 25 34 orim12d
` |-  ( ( dom F i^i dom G ) = (/) -> ( ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) \/ ( ( <. x , y >. e. G /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) \/ ( ( <. x , y >. e. G /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) )`
37 11 36 syl5bi
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) ) )`
38 dffun4
` |-  ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )`
39 38 simprbi
` |-  ( Fun F -> A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )`
40 39 19.21bi
` |-  ( Fun F -> A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )`
41 40 19.21bbi
` |-  ( Fun F -> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )`
42 dffun4
` |-  ( Fun G <-> ( Rel G /\ A. x A. y A. z ( ( <. x , y >. e. G /\ <. x , z >. e. G ) -> y = z ) ) )`
43 42 simprbi
` |-  ( Fun G -> A. x A. y A. z ( ( <. x , y >. e. G /\ <. x , z >. e. G ) -> y = z ) )`
44 43 19.21bi
` |-  ( Fun G -> A. y A. z ( ( <. x , y >. e. G /\ <. x , z >. e. G ) -> y = z ) )`
45 44 19.21bbi
` |-  ( Fun G -> ( ( <. x , y >. e. G /\ <. x , z >. e. G ) -> y = z ) )`
46 41 45 jaao
` |-  ( ( Fun F /\ Fun G ) -> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) -> y = z ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) \/ ( <. x , y >. e. G /\ <. x , z >. e. G ) ) -> y = z ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) -> y = z ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> A. z ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) -> y = z ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> A. x A. y A. z ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) -> y = z ) )`
` |-  ( Fun ( F u. G ) <-> ( Rel ( F u. G ) /\ A. x A. y A. z ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) -> y = z ) ) )`
` |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )`