# Metamath Proof Explorer

## Theorem clsss2

Description: If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007)

Ref Expression
Hypothesis clscld.1
`|- X = U. J`
Assertion clsss2
`|- ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> ( ( cls ` J ) ` S ) C_ C )`

### Proof

Step Hyp Ref Expression
1 clscld.1
` |-  X = U. J`
2 cldrcl
` |-  ( C e. ( Clsd ` J ) -> J e. Top )`
` |-  ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> J e. Top )`
4 1 cldss
` |-  ( C e. ( Clsd ` J ) -> C C_ X )`
` |-  ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> C C_ X )`
6 simpr
` |-  ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> S C_ C )`
7 1 clsss
` |-  ( ( J e. Top /\ C C_ X /\ S C_ C ) -> ( ( cls ` J ) ` S ) C_ ( ( cls ` J ) ` C ) )`
8 3 5 6 7 syl3anc
` |-  ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> ( ( cls ` J ) ` S ) C_ ( ( cls ` J ) ` C ) )`
9 cldcls
` |-  ( C e. ( Clsd ` J ) -> ( ( cls ` J ) ` C ) = C )`
` |-  ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> ( ( cls ` J ) ` C ) = C )`
` |-  ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> ( ( cls ` J ) ` S ) C_ C )`