Theorem mrerintcl

Description: The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	mrerintcl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → ( 𝑋 ∩ ∩ 𝑆 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rint0	⊢ ( 𝑆 = ∅ → ( 𝑋 ∩ ∩ 𝑆 ) = 𝑋 )
2	1	adantl	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) ∧ 𝑆 = ∅ ) → ( 𝑋 ∩ ∩ 𝑆 ) = 𝑋 )
3		mre1cl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
4	3	ad2antrr	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) ∧ 𝑆 = ∅ ) → 𝑋 ∈ 𝐶 )
5	2 4	eqeltrd	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) ∧ 𝑆 = ∅ ) → ( 𝑋 ∩ ∩ 𝑆 ) ∈ 𝐶 )
6		simp2	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ 𝐶 )
7		mresspw	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )
8	7	3ad2ant1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → 𝐶 ⊆ 𝒫 𝑋 )
9	6 8	sstrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ 𝒫 𝑋 )
10		simp3	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → 𝑆 ≠ ∅ )
11		rintn0	⊢ ( ( 𝑆 ⊆ 𝒫 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑆 ) = ∩ 𝑆 )
12	9 10 11	syl2anc	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑆 ) = ∩ 𝑆 )
13		mreintcl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ 𝐶 )
14	12 13	eqeltrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑆 ) ∈ 𝐶 )
15	14	3expa	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) ∧ 𝑆 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑆 ) ∈ 𝐶 )
16	5 15	pm2.61dane	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → ( 𝑋 ∩ ∩ 𝑆 ) ∈ 𝐶 )