Theorem cmntrcld

Description: The complement of an interior is closed. (Contributed by NM, 1-Oct-2007) (Proof shortened by OpenAI, 3-Jul-2020)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	cmntrcld	|- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( int ` J ) ` S ) ) e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2	1	ntropn	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J )
3	1	opncld	|- ( ( J e. Top /\ ( ( int ` J ) ` S ) e. J ) -> ( X \ ( ( int ` J ) ` S ) ) e. ( Clsd ` J ) )
4	2 3	syldan	|- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( int ` J ) ` S ) ) e. ( Clsd ` J ) )