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