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

Metamath Proof Explorer

Theorem incld

Description: The intersection of two closed sets is closed. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion incld ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ∩ B ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 intprg ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → ⋂ A B = A ∩ B
2 prnzg ⊢ A ∈ Clsd ⁡ J → A B ≠ ∅
3 prssi ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A B ⊆ Clsd ⁡ J
4 intcld ⊢ A B ≠ ∅ ∧ A B ⊆ Clsd ⁡ J → ⋂ A B ∈ Clsd ⁡ J
5 2 3 4 syl2an2r ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → ⋂ A B ∈ Clsd ⁡ J
6 1 5 eqeltrrd ⊢ A ∈ Clsd ⁡ J ∧ B ∈ Clsd ⁡ J → A ∩ B ∈ Clsd ⁡ J