inopn

Description: The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006)

		Ref	Expression
	Assertion	inopn	$⊢ (J \in Top \land A \in J \land B \in J) \to A \cap B \in J$

Step	Hyp	Ref	Expression
1		istopg	$⊢ J \in Top \to (J \in Top \leftrightarrow (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x \in J \forall y \in J x \cap y \in J))$
2	1	ibi	$⊢ J \in Top \to (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x \in J \forall y \in J x \cap y \in J)$
3	2	simprd	$⊢ J \in Top \to \forall x \in J \forall y \in J x \cap y \in J$
4		ineq1	$⊢ x = A \to x \cap y = A \cap y$
5	4	eleq1d	$⊢ x = A \to (x \cap y \in J \leftrightarrow A \cap y \in J)$
6		ineq2	$⊢ y = B \to A \cap y = A \cap B$
7	6	eleq1d	$⊢ y = B \to (A \cap y \in J \leftrightarrow A \cap B \in J)$
8	5 7	rspc2v	$⊢ (A \in J \land B \in J) \to (\forall x \in J \forall y \in J x \cap y \in J \to A \cap B \in J)$
9	3 8	syl5com	$⊢ J \in Top \to ((A \in J \land B \in J) \to A \cap B \in J)$
10	9	3impib	$⊢ (J \in Top \land A \in J \land B \in J) \to A \cap B \in J$

Metamath Proof Explorer