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

Theorem funun 5453
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 5428 . . . . 5  |-  ( Fun 
F  ->  Rel  F )
2 funrel 5428 . . . . 5  |-  ( Fun 
G  ->  Rel  G )
31, 2anim12i 566 . . . 4  |-  ( ( Fun  F  /\  Fun  G )  ->  ( Rel  F  /\  Rel  G ) )
4 relun 4948 . . . 4  |-  ( Rel  ( F  u.  G
)  <->  ( Rel  F  /\  Rel  G ) )
53, 4sylibr 212 . . 3  |-  ( ( Fun  F  /\  Fun  G )  ->  Rel  ( F  u.  G ) )
65adantr 465 . 2  |-  ( ( ( Fun  F  /\  Fun  G )  /\  ( dom  F  i^i  dom  G
)  =  (/) )  ->  Rel  ( F  u.  G
) )
7 elun 3490 . . . . . . . 8  |-  ( <.
x ,  y >.  e.  ( F  u.  G
)  <->  ( <. x ,  y >.  e.  F  \/  <. x ,  y
>.  e.  G ) )
8 elun 3490 . . . . . . . 8  |-  ( <.
x ,  z >.  e.  ( F  u.  G
)  <->  ( <. x ,  z >.  e.  F  \/  <. x ,  z
>.  e.  G ) )
97, 8anbi12i 697 . . . . . . 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 865 . . . . . . 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 249 . . . . . 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 3714 . . . . . . . . . . . . 13  |-  ( ( dom  F  i^i  dom  G )  =  (/)  <->  A. x
( x  e.  dom  F  ->  -.  x  e.  dom  G ) )
1312biimpi 194 . . . . . . . . . . . 12  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  A. x
( x  e.  dom  F  ->  -.  x  e.  dom  G ) )
141319.21bi 1804 . . . . . . . . . . 11  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  (
x  e.  dom  F  ->  -.  x  e.  dom  G ) )
15 imnan 422 . . . . . . . . . . 11  |-  ( ( x  e.  dom  F  ->  -.  x  e.  dom  G )  <->  -.  ( x  e.  dom  F  /\  x  e.  dom  G ) )
1614, 15sylib 196 . . . . . . . . . 10  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( x  e.  dom  F  /\  x  e.  dom  G ) )
17 vex 2969 . . . . . . . . . . . 12  |-  x  e. 
_V
18 vex 2969 . . . . . . . . . . . 12  |-  y  e. 
_V
1917, 18opeldm 5035 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  e.  F  ->  x  e. 
dom  F )
20 vex 2969 . . . . . . . . . . . 12  |-  z  e. 
_V
2117, 20opeldm 5035 . . . . . . . . . . 11  |-  ( <.
x ,  z >.  e.  G  ->  x  e. 
dom  G )
2219, 21anim12i 566 . . . . . . . . . 10  |-  ( (
<. x ,  y >.  e.  F  /\  <. x ,  z >.  e.  G
)  ->  ( x  e.  dom  F  /\  x  e.  dom  G ) )
2316, 22nsyl 121 . . . . . . . . 9  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( <. x ,  y
>.  e.  F  /\  <. x ,  z >.  e.  G
) )
24 orel2 383 . . . . . . . . 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 115 . . . . . . . . . . 11  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  (
x  e.  dom  G  ->  -.  x  e.  dom  F ) )
27 imnan 422 . . . . . . . . . . 11  |-  ( ( x  e.  dom  G  ->  -.  x  e.  dom  F )  <->  -.  ( x  e.  dom  G  /\  x  e.  dom  F ) )
2826, 27sylib 196 . . . . . . . . . 10  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( x  e.  dom  G  /\  x  e.  dom  F ) )
2917, 18opeldm 5035 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  e.  G  ->  x  e. 
dom  G )
3017, 20opeldm 5035 . . . . . . . . . . 11  |-  ( <.
x ,  z >.  e.  F  ->  x  e. 
dom  F )
3129, 30anim12i 566 . . . . . . . . . 10  |-  ( (
<. x ,  y >.  e.  G  /\  <. x ,  z >.  e.  F
)  ->  ( x  e.  dom  G  /\  x  e.  dom  F ) )
3228, 31nsyl 121 . . . . . . . . 9  |-  ( ( dom  F  i^i  dom  G )  =  (/)  ->  -.  ( <. x ,  y
>.  e.  G  /\  <. x ,  z >.  e.  F
) )
33 orel1 382 . . . . . . . . 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 834 . . . . . . 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 466 . . . . . 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 217 . . . . 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 5423 . . . . . . . . . 10  |-  ( Fun 
F  <->  ( Rel  F  /\  A. x A. y A. z ( ( <.
x ,  y >.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) ) )
3938simprbi 464 . . . . . . . . 9  |-  ( Fun 
F  ->  A. x A. y A. z ( ( <. x ,  y
>.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) )
403919.21bi 1804 . . . . . . . 8  |-  ( Fun 
F  ->  A. y A. z ( ( <.
x ,  y >.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) )
414019.21bbi 1886 . . . . . . 7  |-  ( Fun 
F  ->  ( ( <. x ,  y >.  e.  F  /\  <. x ,  z >.  e.  F
)  ->  y  =  z ) )
42 dffun4 5423 . . . . . . . . . 10  |-  ( Fun 
G  <->  ( Rel  G  /\  A. x A. y A. z ( ( <.
x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) ) )
4342simprbi 464 . . . . . . . . 9  |-  ( Fun 
G  ->  A. x A. y A. z ( ( <. x ,  y
>.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) )
444319.21bi 1804 . . . . . . . 8  |-  ( Fun 
G  ->  A. y A. z ( ( <.
x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) )
454419.21bbi 1886 . . . . . . 7  |-  ( Fun 
G  ->  ( ( <. x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
)  ->  y  =  z ) )
4641, 45jaao 509 . . . . . 6  |-  ( ( Fun  F  /\  Fun  G )  ->  ( (
( <. x ,  y
>.  e.  F  /\  <. x ,  z >.  e.  F
)  \/  ( <.
x ,  y >.  e.  G  /\  <. x ,  z >.  e.  G
) )  ->  y  =  z ) )
4746adantr 465 . . . . 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 44 . . . 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 1685 . . 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 1686 . 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 5423 . 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 664 1  |-  ( ( ( Fun  F  /\  Fun  G )  /\  ( dom  F  i^i  dom  G
)  =  (/) )  ->  Fun  ( F  u.  G
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756    u. cun 3319    i^i cin 3320   (/)c0 3630   <.cop 3876   dom cdm 4832   Rel wrel 4837   Fun wfun 5405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-br 4286  df-opab 4344  df-id 4628  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-fun 5413
This theorem is referenced by:  funprg  5460  funtpg  5461  funtp  5463  fnun  5510  fvun  5754  tfrlem10  6838  sbthlem7  7419  sbthlem8  7420  fodomr  7454  funsnfsupp  7636  axdc3lem4  8614  strlemor1  14257  strleun  14260  wfrlem13  27683  bnj1421  31890
  Copyright terms: Public domain W3C validator