Theorem rintopn

Description: A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypothesis	1open.1	⊢ 𝑋 = ∪ 𝐽
Assertion	rintopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ∧ 𝐴 ∈ Fin ) → ( 𝑋 ∩ ∩ 𝐴 ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		1open.1	⊢ 𝑋 = ∪ 𝐽
2		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
3	2	ineq2i	⊢ ( 𝑋 ∩ ∩ 𝐴 ) = ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝑥 )
4		dfss3	⊢ ( 𝐴 ⊆ 𝐽 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐽 )
5	1	riinopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐽 ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝑥 ) ∈ 𝐽 )
6	5	3com23	⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ Fin ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝑥 ) ∈ 𝐽 )
7	4 6	syl3an2b	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ∧ 𝐴 ∈ Fin ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝑥 ) ∈ 𝐽 )
8	3 7	eqeltrid	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ∧ 𝐴 ∈ Fin ) → ( 𝑋 ∩ ∩ 𝐴 ) ∈ 𝐽 )