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

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