This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion riincld ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 riin0 ⊢ ( 𝐴 = ∅ → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = 𝑋 )
3 2 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 = ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) = 𝑋 )
4 1 topcld ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
5 4 ad2antrr ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 = ∅ ) → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
6 3 5 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 = ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )
7 4 ad2antrr ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ≠ ∅ ) → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
8 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
9 simplr ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ≠ ∅ ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
10 iincld ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
12 incld ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )
13 7 11 12 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )
14 6 13 pm2.61dane ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )