Theorem ntropn

Description: The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2	1	ntrval	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
3		inss1	|- ( J i^i ~P S ) C_ J
4		uniopn	|- ( ( J e. Top /\ ( J i^i ~P S ) C_ J ) -> U. ( J i^i ~P S ) e. J )
5	3 4	mpan2	|- ( J e. Top -> U. ( J i^i ~P S ) e. J )
6	5	adantr	|- ( ( J e. Top /\ S C_ X ) -> U. ( J i^i ~P S ) e. J )
7	2 6	eqeltrd	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J )