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

Metamath Proof Explorer

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 )