Metamath Proof Explorer

Theorem clsval

Description: The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure 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 clsval 
|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )

Proof

Step Hyp Ref Expression
1 iscld.1 
 |-  X = U. J
2 1 clsfval 
 |-  ( J e. Top -> ( cls ` J ) = ( y e. ~P X |-> |^| { x e. ( Clsd ` J ) | y C_ x } ) )
3 2 fveq1d 
 |-  ( J e. Top -> ( ( cls ` J ) ` S ) = ( ( y e. ~P X |-> |^| { x e. ( Clsd ` J ) | y C_ x } ) ` S ) )
4 3 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( ( y e. ~P X |-> |^| { x e. ( Clsd ` J ) | y C_ x } ) ` S ) )
5 eqid 
 |-  ( y e. ~P X |-> |^| { x e. ( Clsd ` J ) | y C_ x } ) = ( y e. ~P X |-> |^| { x e. ( Clsd ` J ) | y C_ x } )
6 sseq1 
 |-  ( y = S -> ( y C_ x <-> S C_ x ) )
7 6 rabbidv 
 |-  ( y = S -> { x e. ( Clsd ` J ) | y C_ x } = { x e. ( Clsd ` J ) | S C_ x } )
8 7 inteqd 
 |-  ( y = S -> |^| { x e. ( Clsd ` J ) | y C_ x } = |^| { x e. ( Clsd ` J ) | S C_ x } )
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 1 topcld 
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
14 sseq2 
 |-  ( x = X -> ( S C_ x <-> S C_ X ) )
15 14 rspcev 
 |-  ( ( X e. ( Clsd ` J ) /\ S C_ X ) -> E. x e. ( Clsd ` J ) S C_ x )
16 13 15 sylan 
 |-  ( ( J e. Top /\ S C_ X ) -> E. x e. ( Clsd ` J ) S C_ x )
17 intexrab 
 |-  ( E. x e. ( Clsd ` J ) S C_ x <-> |^| { x e. ( Clsd ` J ) | S C_ x } e. _V )
18 16 17 sylib 
 |-  ( ( J e. Top /\ S C_ X ) -> |^| { x e. ( Clsd ` J ) | S C_ x } e. _V )
19 5 8 12 18 fvmptd3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( y e. ~P X |-> |^| { x e. ( Clsd ` J ) | y C_ x } ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
20 4 19 eqtrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )