Metamath Proof Explorer

Theorem riincld

Description: An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypothesis clscld.1 ⊢ X = ⋃ J
Assertion riincld ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → X ∩ ⋂ x ∈ A B ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 riin0 ⊢ A = ∅ → X ∩ ⋂ x ∈ A B = X
3 2 adantl ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A = ∅ → X ∩ ⋂ x ∈ A B = X
4 1 topcld ⊢ J ∈ Top → X ∈ Clsd ⁡ J
5 4 ad2antrr ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A = ∅ → X ∈ Clsd ⁡ J
6 3 5 eqeltrd ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A = ∅ → X ∩ ⋂ x ∈ A B ∈ Clsd ⁡ J
7 4 ad2antrr ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A ≠ ∅ → X ∈ Clsd ⁡ J
8 simpr ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A ≠ ∅ → A ≠ ∅
9 simplr ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A ≠ ∅ → ∀ x ∈ A B ∈ Clsd ⁡ J
10 iincld ⊢ A ≠ ∅ ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → ⋂ x ∈ A B ∈ Clsd ⁡ J
11 8 9 10 syl2anc ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A ≠ ∅ → ⋂ x ∈ A B ∈ Clsd ⁡ J
12 incld ⊢ X ∈ Clsd ⁡ J ∧ ⋂ x ∈ A B ∈ Clsd ⁡ J → X ∩ ⋂ x ∈ A B ∈ Clsd ⁡ J
13 7 11 12 syl2anc ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J ∧ A ≠ ∅ → X ∩ ⋂ x ∈ A B ∈ Clsd ⁡ J
14 6 13 pm2.61dane ⊢ J ∈ Top ∧ ∀ x ∈ A B ∈ Clsd ⁡ J → X ∩ ⋂ x ∈ A B ∈ Clsd ⁡ J