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