Metamath Proof Explorer

Theorem mreincl

Description: Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mreincl ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → A ∩ B ∈ C

Proof

Step Hyp Ref Expression
1 intprg ⊢ A ∈ C ∧ B ∈ C → ⋂ A B = A ∩ B
2 1 3adant1 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → ⋂ A B = A ∩ B
3 simp1 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → C ∈ Moore ⁡ X
4 prssi ⊢ A ∈ C ∧ B ∈ C → A B ⊆ C
5 4 3adant1 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → A B ⊆ C
6 prnzg ⊢ A ∈ C → A B ≠ ∅
7 6 3ad2ant2 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → A B ≠ ∅
8 mreintcl ⊢ C ∈ Moore ⁡ X ∧ A B ⊆ C ∧ A B ≠ ∅ → ⋂ A B ∈ C
9 3 5 7 8 syl3anc ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → ⋂ A B ∈ C
10 2 9 eqeltrrd ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ B ∈ C → A ∩ B ∈ C