iinopn

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014)

		Ref	Expression
	Assertion	iinopn	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to ⋂_{x \in A} B \in J$

Proof

Step	Hyp	Ref	Expression
1		simpr3	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to \forall x \in A B \in J$
2		dfiin2g	$⊢ \forall x \in A B \in J \to ⋂_{x \in A} B = ⋂ \{y \| \exists x \in A y = B\}$
3	1 2	syl	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to ⋂_{x \in A} B = ⋂ \{y \| \exists x \in A y = B\}$
4		simpl	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to J \in Top$
5		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
6	5	rnmpt	$⊢ ran (x \in A ⟼ B) = \{y \| \exists x \in A y = B\}$
7	5	fmpt	$⊢ \forall x \in A B \in J \leftrightarrow (x \in A ⟼ B) : A ⟶ J$
8	1 7	sylib	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to (x \in A ⟼ B) : A ⟶ J$
9	8	frnd	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to ran (x \in A ⟼ B) \subseteq J$
10	6 9	eqsstrrid	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to \{y \| \exists x \in A y = B\} \subseteq J$
11	8	fdmd	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to dom (x \in A ⟼ B) = A$
12		simpr2	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to A \neq \emptyset$
13	11 12	eqnetrd	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to dom (x \in A ⟼ B) \neq \emptyset$
14		dm0rn0	$⊢ dom (x \in A ⟼ B) = \emptyset \leftrightarrow ran (x \in A ⟼ B) = \emptyset$
15	6	eqeq1i	$⊢ ran (x \in A ⟼ B) = \emptyset \leftrightarrow \{y \| \exists x \in A y = B\} = \emptyset$
16	14 15	bitri	$⊢ dom (x \in A ⟼ B) = \emptyset \leftrightarrow \{y \| \exists x \in A y = B\} = \emptyset$
17	16	necon3bii	$⊢ dom (x \in A ⟼ B) \neq \emptyset \leftrightarrow \{y \| \exists x \in A y = B\} \neq \emptyset$
18	13 17	sylib	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to \{y \| \exists x \in A y = B\} \neq \emptyset$
19		simpr1	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to A \in Fin$
20		abrexfi	$⊢ A \in Fin \to \{y \| \exists x \in A y = B\} \in Fin$
21	19 20	syl	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to \{y \| \exists x \in A y = B\} \in Fin$
22		fiinopn	$⊢ J \in Top \to ((\{y \| \exists x \in A y = B\} \subseteq J \land \{y \| \exists x \in A y = B\} \neq \emptyset \land \{y \| \exists x \in A y = B\} \in Fin) \to ⋂ \{y \| \exists x \in A y = B\} \in J)$
23	22	imp	$⊢ (J \in Top \land (\{y \| \exists x \in A y = B\} \subseteq J \land \{y \| \exists x \in A y = B\} \neq \emptyset \land \{y \| \exists x \in A y = B\} \in Fin)) \to ⋂ \{y \| \exists x \in A y = B\} \in J$
24	4 10 18 21 23	syl13anc	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to ⋂ \{y \| \exists x \in A y = B\} \in J$
25	3 24	eqeltrd	$⊢ (J \in Top \land (A \in Fin \land A \neq \emptyset \land \forall x \in A B \in J)) \to ⋂_{x \in A} B \in J$

Metamath Proof Explorer

Theorem iinopn

Proof