Theorem ssntr

Description: An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		elin	|- ( O e. ( J i^i ~P S ) <-> ( O e. J /\ O e. ~P S ) )
3		elpwg	|- ( O e. J -> ( O e. ~P S <-> O C_ S ) )
4	3	pm5.32i	|- ( ( O e. J /\ O e. ~P S ) <-> ( O e. J /\ O C_ S ) )
5	2 4	bitr2i	|- ( ( O e. J /\ O C_ S ) <-> O e. ( J i^i ~P S ) )
6		elssuni	|- ( O e. ( J i^i ~P S ) -> O C_ U. ( J i^i ~P S ) )
7	5 6	sylbi	|- ( ( O e. J /\ O C_ S ) -> O C_ U. ( J i^i ~P S ) )
8	7	adantl	|- ( ( ( J e. Top /\ S C_ X ) /\ ( O e. J /\ O C_ S ) ) -> O C_ U. ( J i^i ~P S ) )
9	1	ntrval	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
10	9	adantr	|- ( ( ( J e. Top /\ S C_ X ) /\ ( O e. J /\ O C_ S ) ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
11	8 10	sseqtrrd	|- ( ( ( J e. Top /\ S C_ X ) /\ ( O e. J /\ O C_ S ) ) -> O C_ ( ( int ` J ) ` S ) )