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 ∈ A B ∈ J → X ∩ ⋂ x ∈ A B ∈ J

Proof

Step Hyp Ref Expression
1 1open.1 ⊢ X = ⋃ J
2 riin0 ⊢ A = ∅ → X ∩ ⋂ x ∈ A B = X
3 2 adantl ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A = ∅ → X ∩ ⋂ x ∈ A B = X
4 simpl1 ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A = ∅ → J ∈ Top
5 1 topopn ⊢ J ∈ Top → X ∈ J
6 4 5 syl ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A = ∅ → X ∈ J
7 3 6 eqeltrd ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A = ∅ → X ∩ ⋂ x ∈ A B ∈ 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 ∈ A B ∈ J → ∀ x ∈ A B ⊆ X
12 11 3impia ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J → ∀ x ∈ A B ⊆ X
13 riinn0 ⊢ ∀ x ∈ A B ⊆ X ∧ A ≠ ∅ → X ∩ ⋂ x ∈ A B = ⋂ x ∈ A B
14 12 13 sylan ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A ≠ ∅ → X ∩ ⋂ x ∈ A B = ⋂ x ∈ A B
15 iinopn ⊢ J ∈ Top ∧ A ∈ Fin ∧ A ≠ ∅ ∧ ∀ x ∈ A B ∈ J → ⋂ x ∈ A B ∈ J
16 15 3exp2 ⊢ J ∈ Top → A ∈ Fin → A ≠ ∅ → ∀ x ∈ A B ∈ J → ⋂ x ∈ A B ∈ J
17 16 com34 ⊢ J ∈ Top → A ∈ Fin → ∀ x ∈ A B ∈ J → A ≠ ∅ → ⋂ x ∈ A B ∈ J
18 17 3imp1 ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A ≠ ∅ → ⋂ x ∈ A B ∈ J
19 14 18 eqeltrd ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J ∧ A ≠ ∅ → X ∩ ⋂ x ∈ A B ∈ J
20 7 19 pm2.61dane ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A B ∈ J → X ∩ ⋂ x ∈ A B ∈ J