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

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

Proof

Step Hyp Ref Expression
1 istopg ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ) ) )
2 1 ibi ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ( 𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ) )
3 2 simprd ⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
4 ineq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝐴 ∩ 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ↔ ( 𝐴 ∩ 𝑦 ) ∈ 𝐽 ) )
6 ineq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ 𝐵 ) )
7 6 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∩ 𝑦 ) ∈ 𝐽 ↔ ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 ) )
8 5 7 rspc2v ⊢ ( ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 ) )
9 3 8 syl5com ⊢ ( 𝐽 ∈ Top → ( ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 ) )
10 9 3impib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )