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	$⊢ \underline{Ⅎ} x C$
	eliuniin2.2	$⊢ A = ⋃_{x \in B} ⋂_{y \in C} D$
Assertion	eliuniin2	$⊢ C \neq \emptyset \to (Z \in A \leftrightarrow \exists x \in B \forall y \in C Z \in D)$

Proof

Step	Hyp	Ref	Expression
1		eliuniin2.1	$⊢ \underline{Ⅎ} x C$
2		eliuniin2.2	$⊢ A = ⋃_{x \in B} ⋂_{y \in C} D$
3	2	eleq2i	$⊢ Z \in A \leftrightarrow Z \in ⋃_{x \in B} ⋂_{y \in C} D$
4		eliun	$⊢ Z \in ⋃_{x \in B} ⋂_{y \in C} D \leftrightarrow \exists x \in B Z \in ⋂_{y \in C} D$
5	3 4	sylbb	$⊢ Z \in A \to \exists x \in B Z \in ⋂_{y \in C} D$
6		eliin	$⊢ Z \in ⋂_{y \in C} D \to (Z \in ⋂_{y \in C} D \leftrightarrow \forall y \in C Z \in D)$
7	6	ibi	$⊢ Z \in ⋂_{y \in C} D \to \forall y \in C Z \in D$
8	7	a1i	$⊢ Z \in A \to (Z \in ⋂_{y \in C} D \to \forall y \in C Z \in D)$
9	8	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)$
10	5 9	mpd	$⊢ Z \in A \to \exists x \in B \forall y \in C Z \in D$
11		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
12	1 11	nfne	$⊢ Ⅎ x C \neq \emptyset$
13		nfv	$⊢ Ⅎ x Z \in A$
14		simp2	$⊢ (C \neq \emptyset \land x \in B \land \forall y \in C Z \in D) \to x \in B$
15		eliin2	$⊢ C \neq \emptyset \to (Z \in ⋂_{y \in C} D \leftrightarrow \forall y \in C Z \in D)$
16	15	biimpar	$⊢ (C \neq \emptyset \land \forall y \in C Z \in D) \to Z \in ⋂_{y \in C} D$
17		rspe	$⊢ (x \in B \land Z \in ⋂_{y \in C} D) \to \exists x \in B Z \in ⋂_{y \in C} D$
18	14 16 17	3imp3i2an	$⊢ (C \neq \emptyset \land x \in B \land \forall y \in C Z \in D) \to \exists x \in B Z \in ⋂_{y \in C} D$
19	18 4	sylibr	$⊢ (C \neq \emptyset \land x \in B \land \forall y \in C Z \in D) \to Z \in ⋃_{x \in B} ⋂_{y \in C} D$
20	19 3	sylibr	$⊢ (C \neq \emptyset \land x \in B \land \forall y \in C Z \in D) \to Z \in A$
21	20	3exp	$⊢ C \neq \emptyset \to (x \in B \to (\forall y \in C Z \in D \to Z \in A))$
22	12 13 21	rexlimd	$⊢ C \neq \emptyset \to (\exists x \in B \forall y \in C Z \in D \to Z \in A)$
23	10 22	impbid2	$⊢ C \neq \emptyset \to (Z \in A \leftrightarrow \exists x \in B \forall y \in C Z \in D)$

Metamath Proof Explorer

Theorem eliuniin2

Proof