mreiincl

Description: A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015)

		Ref	Expression
	Assertion	mreiincl	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to ⋂_{y \in I} S \in C$

Proof

Step	Hyp	Ref	Expression
1		dfiin2g	$⊢ \forall y \in I S \in C \to ⋂_{y \in I} S = ⋂ \{s \| \exists y \in I s = S\}$
2	1	3ad2ant3	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to ⋂_{y \in I} S = ⋂ \{s \| \exists y \in I s = S\}$
3		simp1	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to C \in Moore (X)$
4		uniiunlem	$⊢ \forall y \in I S \in C \to (\forall y \in I S \in C \leftrightarrow \{s \| \exists y \in I s = S\} \subseteq C)$
5	4	ibi	$⊢ \forall y \in I S \in C \to \{s \| \exists y \in I s = S\} \subseteq C$
6	5	3ad2ant3	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to \{s \| \exists y \in I s = S\} \subseteq C$
7		n0	$⊢ I \neq \emptyset \leftrightarrow \exists y y \in I$
8		nfra1	$⊢ Ⅎ y \forall y \in I S \in C$
9		nfre1	$⊢ Ⅎ y \exists y \in I s = S$
10	9	nfab	$⊢ \underline{Ⅎ} y \{s \| \exists y \in I s = S\}$
11		nfcv	$⊢ \underline{Ⅎ} y \emptyset$
12	10 11	nfne	$⊢ Ⅎ y \{s \| \exists y \in I s = S\} \neq \emptyset$
13	8 12	nfim	$⊢ Ⅎ y (\forall y \in I S \in C \to \{s \| \exists y \in I s = S\} \neq \emptyset)$
14		rsp	$⊢ \forall y \in I S \in C \to (y \in I \to S \in C)$
15	14	com12	$⊢ y \in I \to (\forall y \in I S \in C \to S \in C)$
16		elisset	$⊢ S \in C \to \exists s s = S$
17		rspe	$⊢ (y \in I \land \exists s s = S) \to \exists y \in I \exists s s = S$
18	17	ex	$⊢ y \in I \to (\exists s s = S \to \exists y \in I \exists s s = S)$
19	16 18	syl5	$⊢ y \in I \to (S \in C \to \exists y \in I \exists s s = S)$
20		rexcom4	$⊢ \exists y \in I \exists s s = S \leftrightarrow \exists s \exists y \in I s = S$
21	19 20	imbitrdi	$⊢ y \in I \to (S \in C \to \exists s \exists y \in I s = S)$
22	15 21	syld	$⊢ y \in I \to (\forall y \in I S \in C \to \exists s \exists y \in I s = S)$
23		abn0	$⊢ \{s \| \exists y \in I s = S\} \neq \emptyset \leftrightarrow \exists s \exists y \in I s = S$
24	22 23	imbitrrdi	$⊢ y \in I \to (\forall y \in I S \in C \to \{s \| \exists y \in I s = S\} \neq \emptyset)$
25	13 24	exlimi	$⊢ \exists y y \in I \to (\forall y \in I S \in C \to \{s \| \exists y \in I s = S\} \neq \emptyset)$
26	7 25	sylbi	$⊢ I \neq \emptyset \to (\forall y \in I S \in C \to \{s \| \exists y \in I s = S\} \neq \emptyset)$
27	26	imp	$⊢ (I \neq \emptyset \land \forall y \in I S \in C) \to \{s \| \exists y \in I s = S\} \neq \emptyset$
28	27	3adant1	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to \{s \| \exists y \in I s = S\} \neq \emptyset$
29		mreintcl	$⊢ (C \in Moore (X) \land \{s \| \exists y \in I s = S\} \subseteq C \land \{s \| \exists y \in I s = S\} \neq \emptyset) \to ⋂ \{s \| \exists y \in I s = S\} \in C$
30	3 6 28 29	syl3anc	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to ⋂ \{s \| \exists y \in I s = S\} \in C$
31	2 30	eqeltrd	$⊢ (C \in Moore (X) \land I \neq \emptyset \land \forall y \in I S \in C) \to ⋂_{y \in I} S \in C$

Metamath Proof Explorer

Theorem mreiincl

Proof