Theorem inopnd

Description: The intersection of two open sets of a topology is an open set. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	inopnd.1	$$⊢\phi \to J\in \mathrm{Top}$$
	inopnd.2	$$⊢\phi \to A\in J$$
	inopnd.3	$$⊢\phi \to B\in J$$
Assertion	inopnd	$$⊢\phi \to A\cap B\in J$$

Proof

Step	Hyp	Ref	Expression
1		inopnd.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		inopnd.2	$$⊢\phi \to A\in J$$
3		inopnd.3	$$⊢\phi \to B\in J$$
4		inopn	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to A\cap B\in J$$
5	1 2 3 4	syl3anc	$$⊢\phi \to A\cap B\in J$$