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 ) )
6 5 adantr
 |-  ( ( ( 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 ) ) ) )
36 35 adantl
 |-  ( ( ( 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 ) )
47 46 adantr
 |-  ( ( ( 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 ) )
48 37 47 syld
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( <. x , y >. e. ( F u. G ) /\ <. x , z >. e. ( F u. G ) ) -> y = z ) )
49 48 alrimiv
 |-  ( ( ( 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 ) )
50 49 alrimivv
 |-  ( ( ( 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 ) )
51 dffun4
 |-  ( 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 ) ) )
52 6 50 51 sylanbrc
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )