Theorem ntrval

Description: The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of Munkres p. 94. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	iscld.1	|- X = U. J
Assertion	ntrval	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2	1	ntrfval	|- ( J e. Top -> ( int ` J ) = ( x e. ~P X |-> U. ( J i^i ~P x ) ) )
3	2	fveq1d	|- ( J e. Top -> ( ( int ` J ) ` S ) = ( ( x e. ~P X |-> U. ( J i^i ~P x ) ) ` S ) )
4	3	adantr	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = ( ( x e. ~P X |-> U. ( J i^i ~P x ) ) ` S ) )
5		eqid	|- ( x e. ~P X |-> U. ( J i^i ~P x ) ) = ( x e. ~P X |-> U. ( J i^i ~P x ) )
6		pweq	|- ( x = S -> ~P x = ~P S )
7	6	ineq2d	|- ( x = S -> ( J i^i ~P x ) = ( J i^i ~P S ) )
8	7	unieqd	|- ( x = S -> U. ( J i^i ~P x ) = U. ( J i^i ~P S ) )
9	1	topopn	|- ( J e. Top -> X e. J )
10		elpw2g	|- ( X e. J -> ( S e. ~P X <-> S C_ X ) )
11	9 10	syl	|- ( J e. Top -> ( S e. ~P X <-> S C_ X ) )
12	11	biimpar	|- ( ( J e. Top /\ S C_ X ) -> S e. ~P X )
13		inex1g	|- ( J e. Top -> ( J i^i ~P S ) e. _V )
14	13	adantr	|- ( ( J e. Top /\ S C_ X ) -> ( J i^i ~P S ) e. _V )
15	14	uniexd	|- ( ( J e. Top /\ S C_ X ) -> U. ( J i^i ~P S ) e. _V )
16	5 8 12 15	fvmptd3	|- ( ( J e. Top /\ S C_ X ) -> ( ( x e. ~P X |-> U. ( J i^i ~P x ) ) ` S ) = U. ( J i^i ~P S ) )
17	4 16	eqtrd	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )