Theorem 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	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to A\cap B\in J$$

Proof

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