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

Theorem coiun 5348
Description: Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
Assertion
Ref Expression
coiun  |-  ( A  o.  U_ x  e.  C  B )  = 
U_ x  e.  C  ( A  o.  B
)
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem coiun
Dummy variables  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5336 . 2  |-  Rel  ( A  o.  U_ x  e.  C  B )
2 reliun 4957 . . 3  |-  ( Rel  U_ x  e.  C  ( A  o.  B
)  <->  A. x  e.  C  Rel  ( A  o.  B
) )
3 relco 5336 . . . 4  |-  Rel  ( A  o.  B )
43a1i 11 . . 3  |-  ( x  e.  C  ->  Rel  ( A  o.  B
) )
52, 4mprgbir 2754 . 2  |-  Rel  U_ x  e.  C  ( A  o.  B )
6 eliun 4286 . . . . . . . 8  |-  ( <.
y ,  w >.  e. 
U_ x  e.  C  B 
<->  E. x  e.  C  <. y ,  w >.  e.  B )
7 df-br 4406 . . . . . . . 8  |-  ( y
U_ x  e.  C  B w  <->  <. y ,  w >.  e.  U_ x  e.  C  B )
8 df-br 4406 . . . . . . . . 9  |-  ( y B w  <->  <. y ,  w >.  e.  B
)
98rexbii 2891 . . . . . . . 8  |-  ( E. x  e.  C  y B w  <->  E. x  e.  C  <. y ,  w >.  e.  B
)
106, 7, 93bitr4i 281 . . . . . . 7  |-  ( y
U_ x  e.  C  B w  <->  E. x  e.  C  y B w )
1110anbi1i 702 . . . . . 6  |-  ( ( y U_ x  e.  C  B w  /\  w A z )  <->  ( E. x  e.  C  y B w  /\  w A z ) )
12 r19.41v 2944 . . . . . 6  |-  ( E. x  e.  C  ( y B w  /\  w A z )  <->  ( E. x  e.  C  y B w  /\  w A z ) )
1311, 12bitr4i 256 . . . . 5  |-  ( ( y U_ x  e.  C  B w  /\  w A z )  <->  E. x  e.  C  ( y B w  /\  w A z ) )
1413exbii 1720 . . . 4  |-  ( E. w ( y U_ x  e.  C  B w  /\  w A z )  <->  E. w E. x  e.  C  ( y B w  /\  w A z ) )
15 rexcom4 3069 . . . 4  |-  ( E. x  e.  C  E. w ( y B w  /\  w A z )  <->  E. w E. x  e.  C  ( y B w  /\  w A z ) )
1614, 15bitr4i 256 . . 3  |-  ( E. w ( y U_ x  e.  C  B w  /\  w A z )  <->  E. x  e.  C  E. w ( y B w  /\  w A z ) )
17 vex 3050 . . . 4  |-  y  e. 
_V
18 vex 3050 . . . 4  |-  z  e. 
_V
1917, 18opelco 5009 . . 3  |-  ( <.
y ,  z >.  e.  ( A  o.  U_ x  e.  C  B
)  <->  E. w ( y
U_ x  e.  C  B w  /\  w A z ) )
20 eliun 4286 . . . 4  |-  ( <.
y ,  z >.  e.  U_ x  e.  C  ( A  o.  B
)  <->  E. x  e.  C  <. y ,  z >.  e.  ( A  o.  B
) )
2117, 18opelco 5009 . . . . 5  |-  ( <.
y ,  z >.  e.  ( A  o.  B
)  <->  E. w ( y B w  /\  w A z ) )
2221rexbii 2891 . . . 4  |-  ( E. x  e.  C  <. y ,  z >.  e.  ( A  o.  B )  <->  E. x  e.  C  E. w ( y B w  /\  w A z ) )
2320, 22bitri 253 . . 3  |-  ( <.
y ,  z >.  e.  U_ x  e.  C  ( A  o.  B
)  <->  E. x  e.  C  E. w ( y B w  /\  w A z ) )
2416, 19, 233bitr4i 281 . 2  |-  ( <.
y ,  z >.  e.  ( A  o.  U_ x  e.  C  B
)  <->  <. y ,  z
>.  e.  U_ x  e.  C  ( A  o.  B ) )
251, 5, 24eqrelriiv 4932 1  |-  ( A  o.  U_ x  e.  C  B )  = 
U_ x  e.  C  ( A  o.  B
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    = wceq 1446   E.wex 1665    e. wcel 1889   E.wrex 2740   <.cop 3976   U_ciun 4281   class class class wbr 4405    o. ccom 4841   Rel wrel 4842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-iun 4283  df-br 4406  df-opab 4465  df-xp 4843  df-rel 4844  df-co 4846
This theorem is referenced by:  fparlem3  6903  fparlem4  6904  trclrelexplem  36315  trclfvcom  36327
  Copyright terms: Public domain W3C validator