Metamath Proof Explorer

Theorem iinopn

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Assertion iinopn ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→⋂x∈AB∈J

Proof

Step Hyp Ref Expression
1 simpr3 ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→∀x∈AB∈J
2 dfiin2g ⊢∀x∈AB∈J→⋂x∈AB=⋂y|∃x∈Ay=B
3 1 2 syl ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→⋂x∈AB=⋂y|∃x∈Ay=B
4 simpl ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→J∈Top
5 eqid ⊢x∈A⟼B=x∈A⟼B
6 5 rnmpt ⊢ran⁡x∈A⟼B=y|∃x∈Ay=B
7 5 fmpt ⊢∀x∈AB∈J↔x∈A⟼B:A⟶J
8 1 7 sylib ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→x∈A⟼B:A⟶J
9 8 frnd ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→ran⁡x∈A⟼B⊆J
10 6 9 eqsstrrid ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→y|∃x∈Ay=B⊆J
11 8 fdmd ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→dom⁡x∈A⟼B=A
12 simpr2 ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→A≠∅
13 11 12 eqnetrd ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→dom⁡x∈A⟼B≠∅
14 dm0rn0 ⊢dom⁡x∈A⟼B=∅↔ran⁡x∈A⟼B=∅
15 6 eqeq1i ⊢ran⁡x∈A⟼B=∅↔y|∃x∈Ay=B=∅
16 14 15 bitri ⊢dom⁡x∈A⟼B=∅↔y|∃x∈Ay=B=∅
17 16 necon3bii ⊢dom⁡x∈A⟼B≠∅↔y|∃x∈Ay=B≠∅
18 13 17 sylib ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→y|∃x∈Ay=B≠∅
19 simpr1 ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→A∈Fin
20 abrexfi ⊢A∈Fin→y|∃x∈Ay=B∈Fin
21 19 20 syl ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→y|∃x∈Ay=B∈Fin
22 fiinopn ⊢J∈Top→y|∃x∈Ay=B⊆J∧y|∃x∈Ay=B≠∅∧y|∃x∈Ay=B∈Fin→⋂y|∃x∈Ay=B∈J
23 22 imp ⊢J∈Top∧y|∃x∈Ay=B⊆J∧y|∃x∈Ay=B≠∅∧y|∃x∈Ay=B∈Fin→⋂y|∃x∈Ay=B∈J
24 4 10 18 21 23 syl13anc ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→⋂y|∃x∈Ay=B∈J
25 3 24 eqeltrd ⊢J∈Top∧A∈Fin∧A≠∅∧∀x∈AB∈J→⋂x∈AB∈J