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 ‘ 𝐽 ) )