# Metamath Proof Explorer

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