Metamath Proof Explorer

Theorem eliuniin

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

		Ref	Expression
	Hypothesis	eliuniin.1	$⊢ A = ⋃_{x \in B} ⋂_{y \in C} D$
	Assertion	eliuniin	$⊢ Z \in V \to (Z \in A \leftrightarrow \exists x \in B \forall y \in C Z \in D)$

Proof

Step	Hyp	Ref	Expression
1		eliuniin.1	$⊢ A = ⋃_{x \in B} ⋂_{y \in C} D$
2	1	eleq2i	$⊢ Z \in A \leftrightarrow Z \in ⋃_{x \in B} ⋂_{y \in C} D$
3		eliun	$⊢ Z \in ⋃_{x \in B} ⋂_{y \in C} D \leftrightarrow \exists x \in B Z \in ⋂_{y \in C} D$
4	2 3	sylbb	$⊢ Z \in A \to \exists x \in B Z \in ⋂_{y \in C} D$
5		eliin	$⊢ Z \in ⋂_{y \in C} D \to (Z \in ⋂_{y \in C} D \leftrightarrow \forall y \in C Z \in D)$
6	5	ibi	$⊢ Z \in ⋂_{y \in C} D \to \forall y \in C Z \in D$
7	6	a1i	$⊢ Z \in A \to (Z \in ⋂_{y \in C} D \to \forall y \in C Z \in D)$
8	7	reximdv	$⊢ Z \in A \to (\exists x \in B Z \in ⋂_{y \in C} D \to \exists x \in B \forall y \in C Z \in D)$
9	4 8	mpd	$⊢ Z \in A \to \exists x \in B \forall y \in C Z \in D$
10		simp2	$⊢ (Z \in V \land x \in B \land \forall y \in C Z \in D) \to x \in B$
11		eliin	$⊢ Z \in V \to (Z \in ⋂_{y \in C} D \leftrightarrow \forall y \in C Z \in D)$
12	11	biimpar	$⊢ (Z \in V \land \forall y \in C Z \in D) \to Z \in ⋂_{y \in C} D$
13		rspe	$⊢ (x \in B \land Z \in ⋂_{y \in C} D) \to \exists x \in B Z \in ⋂_{y \in C} D$
14	10 12 13	3imp3i2an	$⊢ (Z \in V \land x \in B \land \forall y \in C Z \in D) \to \exists x \in B Z \in ⋂_{y \in C} D$
15	14 3	sylibr	$⊢ (Z \in V \land x \in B \land \forall y \in C Z \in D) \to Z \in ⋃_{x \in B} ⋂_{y \in C} D$
16	15 2	sylibr	$⊢ (Z \in V \land x \in B \land \forall y \in C Z \in D) \to Z \in A$
17	16	rexlimdv3a	$⊢ Z \in V \to (\exists x \in B \forall y \in C Z \in D \to Z \in A)$
18	9 17	impbid2	$⊢ Z \in V \to (Z \in A \leftrightarrow \exists x \in B \forall y \in C Z \in D)$