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