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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	inopnd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
	inopnd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
Assertion	inopnd	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		inopnd.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		inopnd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
3		inopnd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
4		inopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )