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

Theorem reliun 5123
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 4327 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21releqi 5086 . 2  |-  ( Rel  U_ x  e.  A  B 
<->  Rel  { y  |  E. x  e.  A  y  e.  B }
)
3 df-rel 5006 . 2  |-  ( Rel 
{ y  |  E. x  e.  A  y  e.  B }  <->  { y  |  E. x  e.  A  y  e.  B }  C_  ( _V  X.  _V ) )
4 abss 3569 . . 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 5006 . . . . . 6  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
6 dfss2 3493 . . . . . 6  |-  ( B 
C_  ( _V  X.  _V )  <->  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
75, 6bitri 249 . . . . 5  |-  ( Rel 
B  <->  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V ) ) )
87ralbii 2895 . . . 4  |-  ( A. x  e.  A  Rel  B  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  ( _V  X.  _V )
) )
9 ralcom4 3132 . . . 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 2943 . . . . 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 1620 . . . 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 271 . . 3  |-  ( A. x  e.  A  Rel  B  <->  A. y ( E. x  e.  A  y  e.  B  ->  y  e.  ( _V  X.  _V )
) )
134, 12bitr4i 252 . 2  |-  ( { y  |  E. x  e.  A  y  e.  B }  C_  ( _V 
X.  _V )  <->  A. x  e.  A  Rel  B )
142, 3, 133bitri 271 1  |-  ( Rel  U_ x  e.  A  B 
<-> 
A. x  e.  A  Rel  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377    e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815   _Vcvv 3113    C_ wss 3476   U_ciun 4325    X. cxp 4997   Rel wrel 5004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327  df-rel 5006
This theorem is referenced by:  reluni  5125  eliunxp  5140  opeliunxp2  5141  dfco2  5506  coiun  5517  fsumcom2  13555  imasaddfnlem  14786  imasvscafn  14795  gsum2d2lem  16816  gsum2d2  16817  gsumcom2  16818  dprd2d2  16907  cnextrel  20390  reldv  22101  dfcnv2  27286  cvmliftlem1  28481  fprodcom2  28967  eliunxp2  32218
  Copyright terms: Public domain W3C validator