This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )