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	$$⊢\left(A\in \mathrm{Clsd}\left(J\right)\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\cap B\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		intprg	$$⊢\left(A\in \mathrm{Clsd}\left(J\right)\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap \left\{A,B\right\}=A\cap B$$
2		prnzg	$$⊢A\in \mathrm{Clsd}\left(J\right)\to \left\{A,B\right\}\ne \varnothing$$
3		prssi	$$⊢\left(A\in \mathrm{Clsd}\left(J\right)\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to \left\{A,B\right\}\subseteq \mathrm{Clsd}\left(J\right)$$
4		intcld	$$⊢\left(\left\{A,B\right\}\ne \varnothing \wedge \left\{A,B\right\}\subseteq \mathrm{Clsd}\left(J\right)\right)\to \bigcap \left\{A,B\right\}\in \mathrm{Clsd}\left(J\right)$$
5	2 3 4	syl2an2r	$$⊢\left(A\in \mathrm{Clsd}\left(J\right)\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to \bigcap \left\{A,B\right\}\in \mathrm{Clsd}\left(J\right)$$
6	1 5	eqeltrrd	$$⊢\left(A\in \mathrm{Clsd}\left(J\right)\wedge B\in \mathrm{Clsd}\left(J\right)\right)\to A\cap B\in \mathrm{Clsd}\left(J\right)$$