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

Theorem reliun 4928
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 4030 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21releqi 4893 . 2  |-  ( Rel  U_ x  e.  A  B 
<->  Rel  { y  |  E. x  e.  A  y  e.  B }
)
3 df-rel 4818 . 2  |-  ( Rel 
{ y  |  E. x  e.  A  y  e.  B }  <->  { y  |  E. x  e.  A  y  e.  B }  C_  ( _V  X.  _V ) )
4 abss 3348 . . 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 4818 . . . . . 6  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
6 dfss2 3273 . . . . . 6  |-  ( B 
C_  ( _V  X.  _V )  <->  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
75, 6bitri 241 . . . . 5  |-  ( Rel 
B  <->  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
87ralbii 2666 . . . 4  |-  ( A. x  e.  A  Rel  B  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V )
) )
9 ralcom4 2910 . . . 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 2758 . . . . 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 1572 . . . 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 263 . . 3  |-  ( A. x  e.  A  Rel  B  <->  A. y ( E. x  e.  A  y  e.  B  ->  y  e.  ( _V  X.  _V )
) )
134, 12bitr4i 244 . 2  |-  ( { y  |  E. x  e.  A  y  e.  B }  C_  ( _V 
X.  _V )  <->  A. x  e.  A  Rel  B )
142, 3, 133bitri 263 1  |-  ( Rel  U_ x  e.  A  B 
<-> 
A. x  e.  A  Rel  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    e. wcel 1717   {cab 2366   A.wral 2642   E.wrex 2643   _Vcvv 2892    C_ wss 3256   U_ciun 4028    X. cxp 4809   Rel wrel 4816
This theorem is referenced by:  reluni  4930  eliunxp  4945  opeliunxp2  4946  dfco2  5302  coiun  5312  fsumcom2  12478  imasaddfnlem  13673  imasvscafn  13682  gsum2d2lem  15467  gsum2d2  15468  gsumcom2  15469  dprd2d2  15522  cnextrel  18008  reldv  19617  cvmliftlem1  24744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-rex 2648  df-v 2894  df-in 3263  df-ss 3270  df-iun 4030  df-rel 4818
  Copyright terms: Public domain W3C validator