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 e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A i^i B ) e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		intprg	|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> |^| { A , B } = ( A i^i B ) )
2		prnzg	|- ( A e. ( Clsd ` J ) -> { A , B } =/= (/) )
3		prssi	|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> { A , B } C_ ( Clsd ` J ) )
4		intcld	|- ( ( { A , B } =/= (/) /\ { A , B } C_ ( Clsd ` J ) ) -> |^| { A , B } e. ( Clsd ` J ) )
5	2 3 4	syl2an2r	|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> |^| { A , B } e. ( Clsd ` J ) )
6	1 5	eqeltrrd	|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A i^i B ) e. ( Clsd ` J ) )