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 ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C → X ∩ ⋂ y ∈ I S ∈ C

Proof

Step Hyp Ref Expression
1 riin0 ⊢ I = ∅ → X ∩ ⋂ y ∈ I S = X
2 1 adantl ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I = ∅ → X ∩ ⋂ y ∈ I S = X
3 mre1cl ⊢ C ∈ Moore ⁡ X → X ∈ C
4 3 ad2antrr ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I = ∅ → X ∈ C
5 2 4 eqeltrd ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I = ∅ → X ∩ ⋂ y ∈ I S ∈ C
6 mress ⊢ C ∈ Moore ⁡ X ∧ S ∈ C → S ⊆ X
7 6 ex ⊢ C ∈ Moore ⁡ X → S ∈ C → S ⊆ X
8 7 ralimdv ⊢ C ∈ Moore ⁡ X → ∀ y ∈ I S ∈ C → ∀ y ∈ I S ⊆ X
9 8 imp ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C → ∀ y ∈ I S ⊆ X
10 riinn0 ⊢ ∀ y ∈ I S ⊆ X ∧ I ≠ ∅ → X ∩ ⋂ y ∈ I S = ⋂ y ∈ I S
11 9 10 sylan ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I ≠ ∅ → X ∩ ⋂ y ∈ I S = ⋂ y ∈ I S
12 simpll ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I ≠ ∅ → C ∈ Moore ⁡ X
13 simpr ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I ≠ ∅ → I ≠ ∅
14 simplr ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I ≠ ∅ → ∀ y ∈ I S ∈ C
15 mreiincl ⊢ C ∈ Moore ⁡ X ∧ I ≠ ∅ ∧ ∀ y ∈ I S ∈ C → ⋂ y ∈ I S ∈ C
16 12 13 14 15 syl3anc ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I ≠ ∅ → ⋂ y ∈ I S ∈ C
17 11 16 eqeltrd ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C ∧ I ≠ ∅ → X ∩ ⋂ y ∈ I S ∈ C
18 5 17 pm2.61dane ⊢ C ∈ Moore ⁡ X ∧ ∀ y ∈ I S ∈ C → X ∩ ⋂ y ∈ I S ∈ C