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=⋃J
Assertion riinopn ⊢J∈Top∧A∈Fin∧∀x∈AB∈J→X∩⋂x∈AB∈J

Proof

Step Hyp Ref Expression
1 1open.1 ⊢X=⋃J
2 riin0 ⊢A=∅→X∩⋂x∈AB=X
3 2 adantl ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A=∅→X∩⋂x∈AB=X
4 simpl1 ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A=∅→J∈Top
5 1 topopn ⊢J∈Top→X∈J
6 4 5 syl ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A=∅→X∈J
7 3 6 eqeltrd ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A=∅→X∩⋂x∈AB∈J
8 1 eltopss ⊢J∈Top∧B∈J→B⊆X
9 8 ex ⊢J∈Top→B∈J→B⊆X
10 9 adantr ⊢J∈Top∧A∈Fin→B∈J→B⊆X
11 10 ralimdv ⊢J∈Top∧A∈Fin→∀x∈AB∈J→∀x∈AB⊆X
12 11 3impia ⊢J∈Top∧A∈Fin∧∀x∈AB∈J→∀x∈AB⊆X
13 riinn0 ⊢∀x∈AB⊆X∧A≠∅→X∩⋂x∈AB=⋂x∈AB
14 12 13 sylan ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A≠∅→X∩⋂x∈AB=⋂x∈AB
15 iinopn ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→⋂x∈AB∈J
16 15 3exp2 ⊢J∈Top→A∈Fin→A≠∅→∀x∈AB∈J→⋂x∈AB∈J
17 16 com34 ⊢J∈Top→A∈Fin→∀x∈AB∈J→A≠∅→⋂x∈AB∈J
18 17 3imp1 ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A≠∅→⋂x∈AB∈J
19 14 18 eqeltrd ⊢J∈Top∧A∈Fin∧∀x∈AB∈J∧A≠∅→X∩⋂x∈AB∈J
20 7 19 pm2.61dane ⊢J∈Top∧A∈Fin∧∀x∈AB∈J→X∩⋂x∈AB∈J