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