MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funun Structured version   Unicode version

Theorem funun 5524
Description: The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.)
Assertion
Ref Expression
funun  |-  ( ( ( Fun  F  /\  Fun  G )  /\  ( dom  F  i^i  dom  G
)  =  (/) )  ->  Fun  ( F  u.  G
) )

Proof of Theorem funun
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funrel 5500 . . . . 5  |-  ( Fun 
F  ->  Rel  F )
2 funrel 5500 . . . . 5  |-  ( Fun 
G  ->  Rel  G )
31, 2anim12i 551 . . . 4  |-  ( ( Fun  F  /\  Fun  G )  ->  ( Rel  F  /\  Rel  G ) )
4 relun 5020 . . . 4  |-  ( Rel  ( F  u.  G
)  <->  ( Rel  F  /\  Rel  G ) )
53, 4sylibr 205 . . 3  |-  ( ( Fun  F  /\  Fun  G )  ->  Rel  ( F  u.  G ) )
65adantr 453 . 2  |-  ( ( ( Fun  F  /\  Fun  G )  /\  ( dom  F  i^i  dom  G
)  =  (/) )  ->  Rel  ( F  u.  G
) )
7 elun 3474 . . . . . . . 8  |-  ( <.
x ,  y >.  e.  ( F  u.  G
)  <->  ( <. x ,  y >.  e.  F  \/  <. x ,  y
>.  e.  G ) )
8 elun 3474 . . . . . . . 8  |-  ( <.
x ,  z >.  e.  ( F  u.  G
)  <->  ( <. x ,  z >.  e.  F  \/  <. x ,  z
>.  e.  G ) )
97, 8anbi12i 680 . . . . . . 7  |-  ( (
<. 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 842 . . . . . . 7  |-  ( ( ( <. 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
) ) ) )
119, 10bitri 242 . . . . . 6  |-  ( (
<. 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 3694 . . . . . . . . . . . . 13  |-  ( ( dom  F  i^i  dom  G )  =  (/)  <->  A. x
( x  e.  dom  F  ->  -.  x  e.  dom  G ) )
1312biimpi 188 . . . . . . . . . . . 12  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  A. x
( x  e.  dom  F  ->  -.  x  e.  dom  G ) )
141319.21bi 1776 . . . . . . . . . . 11  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  (
x  e.  dom  F  ->  -.  x  e.  dom  G ) )
15 imnan 413 . . . . . . . . . . 11  |-  ( ( x  e.  dom  F  ->  -.  x  e.  dom  G )  <->  -.  ( x  e.  dom  F  /\  x  e.  dom  G ) )
1614, 15sylib 190 . . . . . . . . . 10  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( x  e.  dom  F  /\  x  e.  dom  G ) )
17 vex 2965 . . . . . . . . . . . 12  |-  x  e. 
_V
18 vex 2965 . . . . . . . . . . . 12  |-  y  e. 
_V
1917, 18opeldm 5102 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  e.  F  ->  x  e. 
dom  F )
20 vex 2965 . . . . . . . . . . . 12  |-  z  e. 
_V
2117, 20opeldm 5102 . . . . . . . . . . 11  |-  ( <.
x ,  z >.  e.  G  ->  x  e. 
dom  G )
2219, 21anim12i 551 . . . . . . . . . 10  |-  ( (
<. x ,  y >.  e.  F  /\  <. x ,  z >.  e.  G
)  ->  ( x  e.  dom  F  /\  x  e.  dom  G ) )
2316, 22nsyl 116 . . . . . . . . 9  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( <. x ,  y
>.  e.  F  /\  <. x ,  z >.  e.  G
) )
24 orel2 374 . . . . . . . . 9  |-  ( -.  ( <. 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
) ) )
2523, 24syl 16 . . . . . . . 8  |-  ( ( 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
) ) )
2614con2d 110 . . . . . . . . . . 11  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  (
x  e.  dom  G  ->  -.  x  e.  dom  F ) )
27 imnan 413 . . . . . . . . . . 11  |-  ( ( x  e.  dom  G  ->  -.  x  e.  dom  F )  <->  -.  ( x  e.  dom  G  /\  x  e.  dom  F ) )
2826, 27sylib 190 . . . . . . . . . 10  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( x  e.  dom  G  /\  x  e.  dom  F ) )
2917, 18opeldm 5102 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  e.  G  ->  x  e. 
dom  G )
3017, 20opeldm 5102 . . . . . . . . . . 11  |-  ( <.
x ,  z >.  e.  F  ->  x  e. 
dom  F )
3129, 30anim12i 551 . . . . . . . . . 10  |-  ( (
<. x ,  y >.  e.  G  /\  <. x ,  z >.  e.  F
)  ->  ( x  e.  dom  G  /\  x  e.  dom  F ) )
3228, 31nsyl 116 . . . . . . . . 9  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( <. x ,  y
>.  e.  G  /\  <. x ,  z >.  e.  F
) )
33 orel1 373 . . . . . . . . 9  |-  ( -.  ( <. 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
) ) )
3432, 33syl 16 . . . . . . . 8  |-  ( ( 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
) ) )
3525, 34orim12d 813 . . . . . . 7  |-  ( ( 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
) ) ) )
3635adantl 454 . . . . . 6  |-  ( ( ( 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
) ) ) )
3711, 36syl5bi 210 . . . . 5  |-  ( ( ( 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 5495 . . . . . . . . . 10  |-  ( Fun 
F  <->  ( Rel  F  /\  A. x A. y A. z ( ( <.
x ,  y >.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) ) )
3938simprbi 452 . . . . . . . . 9  |-  ( Fun 
F  ->  A. x A. y A. z ( ( <. x ,  y
>.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) )
403919.21bi 1776 . . . . . . . 8  |-  ( Fun 
F  ->  A. y A. z ( ( <.
x ,  y >.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) )
414019.21bbi 1890 . . . . . . 7  |-  ( Fun 
F  ->  ( ( <. x ,  y >.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) )
42 dffun4 5495 . . . . . . . . . 10  |-  ( Fun 
G  <->  ( Rel  G  /\  A. x A. y A. z ( ( <.
x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) ) )
4342simprbi 452 . . . . . . . . 9  |-  ( Fun 
G  ->  A. x A. y A. z ( ( <. x ,  y
>.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) )
444319.21bi 1776 . . . . . . . 8  |-  ( Fun 
G  ->  A. y A. z ( ( <.
x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) )
454419.21bbi 1890 . . . . . . 7  |-  ( Fun 
G  ->  ( ( <. x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) )
4641, 45jaao 497 . . . . . 6  |-  ( ( Fun  F  /\  Fun  G )  ->  ( (
( <. x ,  y
>.  e.  F  /\  <. x ,  z >.  e.  F
)  \/  ( <.
x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
) )  ->  y  =  z ) )
4746adantr 453 . . . . 5  |-  ( ( ( 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 ) )
4837, 47syld 43 . . . 4  |-  ( ( ( Fun  F  /\  Fun  G )  /\  ( dom  F  i^i  dom  G
)  =  (/) )  -> 
( ( <. x ,  y >.  e.  ( F  u.  G )  /\  <. x ,  z
>.  e.  ( F  u.  G ) )  -> 
y  =  z ) )
4948alrimiv 1642 . . 3  |-  ( ( ( 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 ) )
5049alrimivv 1643 . 2  |-  ( ( ( 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 5495 . 2  |-  ( 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 ) ) )
526, 50, 51sylanbrc 647 1  |-  ( ( ( Fun  F  /\  Fun  G )  /\  ( dom  F  i^i  dom  G
)  =  (/) )  ->  Fun  ( F  u.  G
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359    /\ wa 360   A.wal 1550    = wceq 1653    e. wcel 1727    u. cun 3304    i^i cin 3305   (/)c0 3613   <.cop 3841   dom cdm 4907   Rel wrel 4912   Fun wfun 5477
This theorem is referenced by:  funprg  5529  funtpg  5530  funtp  5532  fnun  5580  fvun  5822  tfrlem10  6677  sbthlem7  7252  sbthlem8  7253  fodomr  7287  axdc3lem4  8364  strlemor1  13587  strleun  13590  wfrlem13  25581  bnj1421  29509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-br 4238  df-opab 4292  df-id 4527  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-fun 5485
  Copyright terms: Public domain W3C validator