Theorem eliuniin2

Description: Indexed union of indexed intersections. See eliincex for a counterexample showing that the precondition C =/= (/) cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	eliuniin2.1	|- F/_ x C
	eliuniin2.2	|- A = U_ x e. B |^|_ y e. C D
Assertion	eliuniin2	|- ( C =/= (/) -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )

Proof

Step	Hyp	Ref	Expression
1		eliuniin2.1	|- F/_ x C
2		eliuniin2.2	|- A = U_ x e. B |^|_ y e. C D
3	2	eleq2i	|- ( Z e. A <-> Z e. U_ x e. B |^|_ y e. C D )
4		eliun	|- ( Z e. U_ x e. B |^|_ y e. C D <-> E. x e. B Z e. |^|_ y e. C D )
5	3 4	sylbb	|- ( Z e. A -> E. x e. B Z e. |^|_ y e. C D )
6		eliin	|- ( Z e. |^|_ y e. C D -> ( Z e. |^|_ y e. C D <-> A. y e. C Z e. D ) )
7	6	ibi	|- ( Z e. |^|_ y e. C D -> A. y e. C Z e. D )
8	7	a1i	|- ( Z e. A -> ( Z e. |^|_ y e. C D -> A. y e. C Z e. D ) )
9	8	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 ) )
10	5 9	mpd	|- ( Z e. A -> E. x e. B A. y e. C Z e. D )
11		nfcv	|- F/_ x (/)
12	1 11	nfne	|- F/ x C =/= (/)
13		nfv	|- F/ x Z e. A
14		simp2	|- ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> x e. B )
15		eliin2	|- ( C =/= (/) -> ( Z e. |^|_ y e. C D <-> A. y e. C Z e. D ) )
16	15	biimpar	|- ( ( C =/= (/) /\ A. y e. C Z e. D ) -> Z e. |^|_ y e. C D )
17		rspe	|- ( ( x e. B /\ Z e. |^|_ y e. C D ) -> E. x e. B Z e. |^|_ y e. C D )
18	14 16 17	3imp3i2an	|- ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> E. x e. B Z e. |^|_ y e. C D )
19	18 4	sylibr	|- ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> Z e. U_ x e. B |^|_ y e. C D )
20	19 3	sylibr	|- ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> Z e. A )
21	20	3exp	|- ( C =/= (/) -> ( x e. B -> ( A. y e. C Z e. D -> Z e. A ) ) )
22	12 13 21	rexlimd	|- ( C =/= (/) -> ( E. x e. B A. y e. C Z e. D -> Z e. A ) )
23	10 22	impbid2	|- ( C =/= (/) -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )