Theorem mreriincl

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

	Ref	Expression
Assertion	mreriincl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		riin0	⊢ ( 𝐼 = ∅ → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) = 𝑋 )
2	1	adantl	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 = ∅ ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) = 𝑋 )
3		mre1cl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
4	3	ad2antrr	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 = ∅ ) → 𝑋 ∈ 𝐶 )
5	2 4	eqeltrd	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 = ∅ ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) ∈ 𝐶 )
6		mress	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ⊆ 𝑋 )
7	6	ex	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑋 ) )
8	7	ralimdv	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 → ∀ 𝑦 ∈ 𝐼 𝑆 ⊆ 𝑋 ) )
9	8	imp	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) → ∀ 𝑦 ∈ 𝐼 𝑆 ⊆ 𝑋 )
10		riinn0	⊢ ( ( ∀ 𝑦 ∈ 𝐼 𝑆 ⊆ 𝑋 ∧ 𝐼 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) = ∩ 𝑦 ∈ 𝐼 𝑆 )
11	9 10	sylan	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) = ∩ 𝑦 ∈ 𝐼 𝑆 )
12		simpll	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 ≠ ∅ ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
13		simpr	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 ≠ ∅ ) → 𝐼 ≠ ∅ )
14		simplr	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 ≠ ∅ ) → ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 )
15		mreiincl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 )
16	12 13 14 15	syl3anc	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 ≠ ∅ ) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 )
17	11 16	eqeltrd	⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) ∧ 𝐼 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) ∈ 𝐶 )
18	5 17	pm2.61dane	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶 ) → ( 𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆 ) ∈ 𝐶 )