This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iuniin

Description: Law combining indexed union with indexed intersection. Eq. 14 in KuratowskiMostowski p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29 . (Contributed by NM, 17-Aug-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iuniin 
|- U_ x e. A |^|_ y e. B C C_ |^|_ y e. B U_ x e. A C

Proof

Step Hyp Ref Expression
1 r19.12 
 |-  ( E. x e. A A. y e. B z e. C -> A. y e. B E. x e. A z e. C )
2 eliin 
 |-  ( z e. _V -> ( z e. |^|_ y e. B C <-> A. y e. B z e. C ) )
3 2 elv 
 |-  ( z e. |^|_ y e. B C <-> A. y e. B z e. C )
4 3 rexbii 
 |-  ( E. x e. A z e. |^|_ y e. B C <-> E. x e. A A. y e. B z e. C )
5 eliun 
 |-  ( z e. U_ x e. A C <-> E. x e. A z e. C )
6 5 ralbii 
 |-  ( A. y e. B z e. U_ x e. A C <-> A. y e. B E. x e. A z e. C )
7 1 4 6 3imtr4i 
 |-  ( E. x e. A z e. |^|_ y e. B C -> A. y e. B z e. U_ x e. A C )
8 eliun 
 |-  ( z e. U_ x e. A |^|_ y e. B C <-> E. x e. A z e. |^|_ y e. B C )
9 eliin 
 |-  ( z e. _V -> ( z e. |^|_ y e. B U_ x e. A C <-> A. y e. B z e. U_ x e. A C ) )
10 9 elv 
 |-  ( z e. |^|_ y e. B U_ x e. A C <-> A. y e. B z e. U_ x e. A C )
11 7 8 10 3imtr4i 
 |-  ( z e. U_ x e. A |^|_ y e. B C -> z e. |^|_ y e. B U_ x e. A C )
12 11 ssriv 
 |-  U_ x e. A |^|_ y e. B C C_ |^|_ y e. B U_ x e. A C