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 ‘ 𝐽 ) )