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 ) )