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 Clsd J B Clsd J A B Clsd J

Proof

Step Hyp Ref Expression
1 intprg A Clsd J B Clsd J A B = A B
2 prnzg A Clsd J A B
3 prssi A Clsd J B Clsd J A B Clsd J
4 intcld A B A B Clsd J A B Clsd J
5 2 3 4 syl2an2r A Clsd J B Clsd J A B Clsd J
6 1 5 eqeltrrd A Clsd J B Clsd J A B Clsd J