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∈AB∈Clsd⁡J→X∩⋂x∈AB∈Clsd⁡J

Proof

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