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

Metamath Proof Explorer

Theorem mreintcl

Description: A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mreintcl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 elpw2g ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝐶 ↔ 𝑆 ⊆ 𝐶 ) )
2 1 biimpar ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → 𝑆 ∈ 𝒫 𝐶 )
3 2 3adant3 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → 𝑆 ∈ 𝒫 𝐶 )
4 ismre ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) )
5 4 simp3bi ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) )
6 5 3ad2ant1 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) )
7 simp3 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → 𝑆 ≠ ∅ )
8 neeq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ≠ ∅ ↔ 𝑆 ≠ ∅ ) )
9 inteq ⊢ ( 𝑠 = 𝑆 → ∩ 𝑠 = ∩ 𝑆 )
10 9 eleq1d ⊢ ( 𝑠 = 𝑆 → ( ∩ 𝑠 ∈ 𝐶 ↔ ∩ 𝑆 ∈ 𝐶 ) )
11 8 10 imbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ↔ ( 𝑆 ≠ ∅ → ∩ 𝑆 ∈ 𝐶 ) ) )
12 11 rspcva ⊢ ( ( 𝑆 ∈ 𝒫 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) → ( 𝑆 ≠ ∅ → ∩ 𝑆 ∈ 𝐶 ) )
13 12 3impia ⊢ ( ( 𝑆 ∈ 𝒫 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ 𝐶 )
14 3 6 7 13 syl3anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ 𝐶 )