# Metamath Proof Explorer

## 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 ‘ 𝑋 ) ∧ 𝑆𝐶 ) → ( 𝑋 𝑆 ) ∈ 𝐶 )