Metamath Proof Explorer

Theorem fiinopn

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012)

Ref Expression
Assertion fiinopn ⊢J∈Top→A⊆J∧A≠∅∧A∈Fin→⋂A∈J

Proof

Step Hyp Ref Expression
1 elpwg ⊢A∈Fin→A∈𝒫J↔A⊆J
2 sseq1 ⊢x=A→x⊆J↔A⊆J
3 neeq1 ⊢x=A→x≠∅↔A≠∅
4 eleq1 ⊢x=A→x∈Fin↔A∈Fin
5 2 3 4 3anbi123d ⊢x=A→x⊆J∧x≠∅∧x∈Fin↔A⊆J∧A≠∅∧A∈Fin
6 inteq ⊢x=A→⋂x=⋂A
7 6 eleq1d ⊢x=A→⋂x∈J↔⋂A∈J
8 7 imbi2d ⊢x=A→J∈Top→⋂x∈J↔J∈Top→⋂A∈J
9 5 8 imbi12d ⊢x=A→x⊆J∧x≠∅∧x∈Fin→J∈Top→⋂x∈J↔A⊆J∧A≠∅∧A∈Fin→J∈Top→⋂A∈J
10 sp ⊢∀xx⊆J∧x≠∅∧x∈Fin→⋂x∈J→x⊆J∧x≠∅∧x∈Fin→⋂x∈J
11 10 adantl ⊢∀xx⊆J→⋃x∈J∧∀xx⊆J∧x≠∅∧x∈Fin→⋂x∈J→x⊆J∧x≠∅∧x∈Fin→⋂x∈J
12 istop2g ⊢J∈Top→J∈Top↔∀xx⊆J→⋃x∈J∧∀xx⊆J∧x≠∅∧x∈Fin→⋂x∈J
13 12 ibi ⊢J∈Top→∀xx⊆J→⋃x∈J∧∀xx⊆J∧x≠∅∧x∈Fin→⋂x∈J
14 11 13 syl11 ⊢x⊆J∧x≠∅∧x∈Fin→J∈Top→⋂x∈J
15 9 14 vtoclg ⊢A∈𝒫J→A⊆J∧A≠∅∧A∈Fin→J∈Top→⋂A∈J
16 15 com12 ⊢A⊆J∧A≠∅∧A∈Fin→A∈𝒫J→J∈Top→⋂A∈J
17 16 3exp ⊢A⊆J→A≠∅→A∈Fin→A∈𝒫J→J∈Top→⋂A∈J
18 17 com3r ⊢A∈Fin→A⊆J→A≠∅→A∈𝒫J→J∈Top→⋂A∈J
19 18 com4r ⊢A∈𝒫J→A∈Fin→A⊆J→A≠∅→J∈Top→⋂A∈J
20 1 19 syl6bir ⊢A∈Fin→A⊆J→A∈Fin→A⊆J→A≠∅→J∈Top→⋂A∈J
21 20 pm2.43a ⊢A∈Fin→A⊆J→A⊆J→A≠∅→J∈Top→⋂A∈J
22 21 com4l ⊢A⊆J→A⊆J→A≠∅→A∈Fin→J∈Top→⋂A∈J
23 22 pm2.43i ⊢A⊆J→A≠∅→A∈Fin→J∈Top→⋂A∈J
24 23 3imp ⊢A⊆J∧A≠∅∧A∈Fin→J∈Top→⋂A∈J
25 24 com12 ⊢J∈Top→A⊆J∧A≠∅∧A∈Fin→⋂A∈J