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 )