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 ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 intprg ⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
2 prnzg ⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → { 𝐴 , 𝐵 } ≠ ∅ )
3 prssi ⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → { 𝐴 , 𝐵 } ⊆ ( Clsd ‘ 𝐽 ) )
4 intcld ⊢ ( ( { 𝐴 , 𝐵 } ≠ ∅ ∧ { 𝐴 , 𝐵 } ⊆ ( Clsd ‘ 𝐽 ) ) → ∩ { 𝐴 , 𝐵 } ∈ ( Clsd ‘ 𝐽 ) )
5 2 3 4 syl2an2r ⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ { 𝐴 , 𝐵 } ∈ ( Clsd ‘ 𝐽 ) )
6 1 5 eqeltrrd ⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( Clsd ‘ 𝐽 ) )