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 ⊢ φ → J ∈ Top
inopnd.2 ⊢ φ → A ∈ J
inopnd.3 ⊢ φ → B ∈ J
Assertion inopnd ⊢ φ → A ∩ B ∈ J

Proof

Step Hyp Ref Expression
1 inopnd.1 ⊢ φ → J ∈ Top
2 inopnd.2 ⊢ φ → A ∈ J
3 inopnd.3 ⊢ φ → B ∈ J
4 inopn ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → A ∩ B ∈ J
5 1 2 3 4 syl3anc ⊢ φ → A ∩ B ∈ J