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

Metamath Proof Explorer

Theorem rintopn

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

Ref Expression
Hypothesis 1open.1 
|- X = U. J
Assertion rintopn 
|- ( ( J e. Top /\ A C_ J /\ A e. Fin ) -> ( X i^i |^| A ) e. J )

Proof

Step Hyp Ref Expression
1 1open.1 
 |-  X = U. J
2 intiin 
 |-  |^| A = |^|_ x e. A x
3 2 ineq2i 
 |-  ( X i^i |^| A ) = ( X i^i |^|_ x e. A x )
4 dfss3 
 |-  ( A C_ J <-> A. x e. A x e. J )
5 1 riinopn 
 |-  ( ( J e. Top /\ A e. Fin /\ A. x e. A x e. J ) -> ( X i^i |^|_ x e. A x ) e. J )
6 5 3com23 
 |-  ( ( J e. Top /\ A. x e. A x e. J /\ A e. Fin ) -> ( X i^i |^|_ x e. A x ) e. J )
7 4 6 syl3an2b 
 |-  ( ( J e. Top /\ A C_ J /\ A e. Fin ) -> ( X i^i |^|_ x e. A x ) e. J )
8 3 7 eqeltrid 
 |-  ( ( J e. Top /\ A C_ J /\ A e. Fin ) -> ( X i^i |^| A ) e. J )