Metamath Proof Explorer

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 ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → A ∩ B ∈ J

Proof

Step Hyp Ref Expression
1 istopg ⊢ J ∈ Top → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
2 1 ibi ⊢ J ∈ Top → ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
3 2 simprd ⊢ J ∈ Top → ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
4 ineq1 ⊢ x = A → x ∩ y = A ∩ y
5 4 eleq1d ⊢ x = A → x ∩ y ∈ J ↔ A ∩ y ∈ J
6 ineq2 ⊢ y = B → A ∩ y = A ∩ B
7 6 eleq1d ⊢ y = B → A ∩ y ∈ J ↔ A ∩ B ∈ J
8 5 7 rspc2v ⊢ A ∈ J ∧ B ∈ J → ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J → A ∩ B ∈ J
9 3 8 syl5com ⊢ J ∈ Top → A ∈ J ∧ B ∈ J → A ∩ B ∈ J
10 9 3impib ⊢ J ∈ Top ∧ A ∈ J ∧ B ∈ J → A ∩ B ∈ J