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 ⊢ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J → x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J
11 10 adantl ⊢ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J → x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J
12 istop2g ⊢ J ∈ Top → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J
13 12 ibi ⊢ J ∈ Top → ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x x ⊆ 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 biimtrrdi ⊢ 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