Theorem riinopn

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

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

Proof

Step	Hyp	Ref	Expression
1		1open.1	|- X = U. J
2		riin0	|- ( A = (/) -> ( X i^i |^|_ x e. A B ) = X )
3	2	adantl	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A = (/) ) -> ( X i^i |^|_ x e. A B ) = X )
4		simpl1	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A = (/) ) -> J e. Top )
5	1	topopn	|- ( J e. Top -> X e. J )
6	4 5	syl	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A = (/) ) -> X e. J )
7	3 6	eqeltrd	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A = (/) ) -> ( X i^i |^|_ x e. A B ) e. J )
8	1	eltopss	|- ( ( J e. Top /\ B e. J ) -> B C_ X )
9	8	ex	|- ( J e. Top -> ( B e. J -> B C_ X ) )
10	9	adantr	|- ( ( J e. Top /\ A e. Fin ) -> ( B e. J -> B C_ X ) )
11	10	ralimdv	|- ( ( J e. Top /\ A e. Fin ) -> ( A. x e. A B e. J -> A. x e. A B C_ X ) )
12	11	3impia	|- ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) -> A. x e. A B C_ X )
13		riinn0	|- ( ( A. x e. A B C_ X /\ A =/= (/) ) -> ( X i^i |^|_ x e. A B ) = |^|_ x e. A B )
14	12 13	sylan	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A =/= (/) ) -> ( X i^i |^|_ x e. A B ) = |^|_ x e. A B )
15		iinopn	|- ( ( J e. Top /\ ( A e. Fin /\ A =/= (/) /\ A. x e. A B e. J ) ) -> |^|_ x e. A B e. J )
16	15	3exp2	|- ( J e. Top -> ( A e. Fin -> ( A =/= (/) -> ( A. x e. A B e. J -> |^|_ x e. A B e. J ) ) ) )
17	16	com34	|- ( J e. Top -> ( A e. Fin -> ( A. x e. A B e. J -> ( A =/= (/) -> |^|_ x e. A B e. J ) ) ) )
18	17	3imp1	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A =/= (/) ) -> |^|_ x e. A B e. J )
19	14 18	eqeltrd	|- ( ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) /\ A =/= (/) ) -> ( X i^i |^|_ x e. A B ) e. J )
20	7 19	pm2.61dane	|- ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. J ) -> ( X i^i |^|_ x e. A B ) e. J )