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

Metamath Proof Explorer

Theorem eliuniin

Description: Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis eliuniin.1 
|- A = U_ x e. B |^|_ y e. C D
Assertion eliuniin 
|- ( Z e. V -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )

Proof

Step Hyp Ref Expression
1 eliuniin.1 
 |-  A = U_ x e. B |^|_ y e. C D
2 1 eleq2i 
 |-  ( Z e. A <-> Z e. U_ x e. B |^|_ y e. C D )
3 eliun 
 |-  ( Z e. U_ x e. B |^|_ y e. C D <-> E. x e. B Z e. |^|_ y e. C D )
4 2 3 sylbb 
 |-  ( Z e. A -> E. x e. B Z e. |^|_ y e. C D )
5 eliin 
 |-  ( Z e. |^|_ y e. C D -> ( Z e. |^|_ y e. C D <-> A. y e. C Z e. D ) )
6 5 ibi 
 |-  ( Z e. |^|_ y e. C D -> A. y e. C Z e. D )
7 6 a1i 
 |-  ( Z e. A -> ( Z e. |^|_ y e. C D -> A. y e. C Z e. D ) )
8 7 reximdv 
 |-  ( Z e. A -> ( E. x e. B Z e. |^|_ y e. C D -> E. x e. B A. y e. C Z e. D ) )
9 4 8 mpd 
 |-  ( Z e. A -> E. x e. B A. y e. C Z e. D )
10 simp2 
 |-  ( ( Z e. V /\ x e. B /\ A. y e. C Z e. D ) -> x e. B )
11 eliin 
 |-  ( Z e. V -> ( Z e. |^|_ y e. C D <-> A. y e. C Z e. D ) )
12 11 biimpar 
 |-  ( ( Z e. V /\ A. y e. C Z e. D ) -> Z e. |^|_ y e. C D )
13 rspe 
 |-  ( ( x e. B /\ Z e. |^|_ y e. C D ) -> E. x e. B Z e. |^|_ y e. C D )
14 10 12 13 3imp3i2an 
 |-  ( ( Z e. V /\ x e. B /\ A. y e. C Z e. D ) -> E. x e. B Z e. |^|_ y e. C D )
15 14 3 sylibr 
 |-  ( ( Z e. V /\ x e. B /\ A. y e. C Z e. D ) -> Z e. U_ x e. B |^|_ y e. C D )
16 15 2 sylibr 
 |-  ( ( Z e. V /\ x e. B /\ A. y e. C Z e. D ) -> Z e. A )
17 16 rexlimdv3a 
 |-  ( Z e. V -> ( E. x e. B A. y e. C Z e. D -> Z e. A ) )
18 9 17 impbid2 
 |-  ( Z e. V -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )