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

Theorem reliun 4974
Description: An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
Assertion
Ref Expression
reliun  |-  ( Rel  U_ x  e.  A  B 
<-> 
A. x  e.  A  Rel  B )

Proof of Theorem reliun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-iun 4304 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21releqi 4938 . 2  |-  ( Rel  U_ x  e.  A  B 
<->  Rel  { y  |  E. x  e.  A  y  e.  B }
)
3 df-rel 4861 . 2  |-  ( Rel 
{ y  |  E. x  e.  A  y  e.  B }  <->  { y  |  E. x  e.  A  y  e.  B }  C_  ( _V  X.  _V ) )
4 abss 3536 . . 3  |-  ( { y  |  E. x  e.  A  y  e.  B }  C_  ( _V 
X.  _V )  <->  A. y
( E. x  e.  A  y  e.  B  ->  y  e.  ( _V 
X.  _V ) ) )
5 df-rel 4861 . . . . . 6  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
6 dfss2 3459 . . . . . 6  |-  ( B 
C_  ( _V  X.  _V )  <->  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
75, 6bitri 252 . . . . 5  |-  ( Rel 
B  <->  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
87ralbii 2863 . . . 4  |-  ( A. x  e.  A  Rel  B  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V )
) )
9 ralcom4 3106 . . . 4  |-  ( A. x  e.  A  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V )
)  <->  A. y A. x  e.  A  ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
10 r19.23v 2912 . . . . 5  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  ( _V 
X.  _V ) )  <->  ( E. x  e.  A  y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
1110albii 1687 . . . 4  |-  ( A. y A. x  e.  A  ( y  e.  B  ->  y  e.  ( _V 
X.  _V ) )  <->  A. y
( E. x  e.  A  y  e.  B  ->  y  e.  ( _V 
X.  _V ) ) )
128, 9, 113bitri 274 . . 3  |-  ( A. x  e.  A  Rel  B  <->  A. y ( E. x  e.  A  y  e.  B  ->  y  e.  ( _V  X.  _V )
) )
134, 12bitr4i 255 . 2  |-  ( { y  |  E. x  e.  A  y  e.  B }  C_  ( _V 
X.  _V )  <->  A. x  e.  A  Rel  B )
142, 3, 133bitri 274 1  |-  ( Rel  U_ x  e.  A  B 
<-> 
A. x  e.  A  Rel  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    e. wcel 1870   {cab 2414   A.wral 2782   E.wrex 2783   _Vcvv 3087    C_ wss 3442   U_ciun 4302    X. cxp 4852   Rel wrel 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-v 3089  df-in 3449  df-ss 3456  df-iun 4304  df-rel 4861
This theorem is referenced by:  reluni  4976  eliunxp  4992  opeliunxp2  4993  dfco2  5354  coiun  5365  fvn0ssdmfun  6028  fsumcom2  13813  fprodcom2  14016  imasaddfnlem  15385  imasvscafn  15394  gsum2d2lem  17540  gsum2d2  17541  gsumcom2  17542  dprd2d2  17612  cnextrel  21009  reldv  22702  dfcnv2  28119  cvmliftlem1  29796  cnviun  35884  coiun1  35886  eliunxp2  38887
  Copyright terms: Public domain W3C validator