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

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