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 ) )