This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )