Metamath Proof Explorer


Theorem clsval2

Description: Express closure in terms of interior. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 clscld.1
 |-  X = U. J
2 df-rab
 |-  { z e. ( Clsd ` J ) | S C_ z } = { z | ( z e. ( Clsd ` J ) /\ S C_ z ) }
3 1 cldopn
 |-  ( z e. ( Clsd ` J ) -> ( X \ z ) e. J )
4 3 ad2antrl
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> ( X \ z ) e. J )
5 sscon
 |-  ( S C_ z -> ( X \ z ) C_ ( X \ S ) )
6 5 ad2antll
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> ( X \ z ) C_ ( X \ S ) )
7 1 topopn
 |-  ( J e. Top -> X e. J )
8 difexg
 |-  ( X e. J -> ( X \ z ) e. _V )
9 elpwg
 |-  ( ( X \ z ) e. _V -> ( ( X \ z ) e. ~P ( X \ S ) <-> ( X \ z ) C_ ( X \ S ) ) )
10 7 8 9 3syl
 |-  ( J e. Top -> ( ( X \ z ) e. ~P ( X \ S ) <-> ( X \ z ) C_ ( X \ S ) ) )
11 10 ad2antrr
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> ( ( X \ z ) e. ~P ( X \ S ) <-> ( X \ z ) C_ ( X \ S ) ) )
12 6 11 mpbird
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> ( X \ z ) e. ~P ( X \ S ) )
13 4 12 elind
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> ( X \ z ) e. ( J i^i ~P ( X \ S ) ) )
14 1 cldss
 |-  ( z e. ( Clsd ` J ) -> z C_ X )
15 14 ad2antrl
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> z C_ X )
16 dfss4
 |-  ( z C_ X <-> ( X \ ( X \ z ) ) = z )
17 15 16 sylib
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> ( X \ ( X \ z ) ) = z )
18 17 eqcomd
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> z = ( X \ ( X \ z ) ) )
19 difeq2
 |-  ( x = ( X \ z ) -> ( X \ x ) = ( X \ ( X \ z ) ) )
20 19 rspceeqv
 |-  ( ( ( X \ z ) e. ( J i^i ~P ( X \ S ) ) /\ z = ( X \ ( X \ z ) ) ) -> E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) )
21 13 18 20 syl2anc
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( z e. ( Clsd ` J ) /\ S C_ z ) ) -> E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) )
22 21 ex
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( z e. ( Clsd ` J ) /\ S C_ z ) -> E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) ) )
23 simpl
 |-  ( ( J e. Top /\ S C_ X ) -> J e. Top )
24 elinel1
 |-  ( x e. ( J i^i ~P ( X \ S ) ) -> x e. J )
25 1 opncld
 |-  ( ( J e. Top /\ x e. J ) -> ( X \ x ) e. ( Clsd ` J ) )
26 23 24 25 syl2an
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> ( X \ x ) e. ( Clsd ` J ) )
27 elinel2
 |-  ( x e. ( J i^i ~P ( X \ S ) ) -> x e. ~P ( X \ S ) )
28 27 adantl
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> x e. ~P ( X \ S ) )
29 28 elpwid
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> x C_ ( X \ S ) )
30 29 difss2d
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> x C_ X )
31 simplr
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> S C_ X )
32 ssconb
 |-  ( ( x C_ X /\ S C_ X ) -> ( x C_ ( X \ S ) <-> S C_ ( X \ x ) ) )
33 30 31 32 syl2anc
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> ( x C_ ( X \ S ) <-> S C_ ( X \ x ) ) )
34 29 33 mpbid
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> S C_ ( X \ x ) )
35 26 34 jca
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> ( ( X \ x ) e. ( Clsd ` J ) /\ S C_ ( X \ x ) ) )
36 eleq1
 |-  ( z = ( X \ x ) -> ( z e. ( Clsd ` J ) <-> ( X \ x ) e. ( Clsd ` J ) ) )
37 sseq2
 |-  ( z = ( X \ x ) -> ( S C_ z <-> S C_ ( X \ x ) ) )
38 36 37 anbi12d
 |-  ( z = ( X \ x ) -> ( ( z e. ( Clsd ` J ) /\ S C_ z ) <-> ( ( X \ x ) e. ( Clsd ` J ) /\ S C_ ( X \ x ) ) ) )
39 35 38 syl5ibrcom
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( J i^i ~P ( X \ S ) ) ) -> ( z = ( X \ x ) -> ( z e. ( Clsd ` J ) /\ S C_ z ) ) )
40 39 rexlimdva
 |-  ( ( J e. Top /\ S C_ X ) -> ( E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) -> ( z e. ( Clsd ` J ) /\ S C_ z ) ) )
41 22 40 impbid
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( z e. ( Clsd ` J ) /\ S C_ z ) <-> E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) ) )
42 41 abbidv
 |-  ( ( J e. Top /\ S C_ X ) -> { z | ( z e. ( Clsd ` J ) /\ S C_ z ) } = { z | E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) } )
43 2 42 syl5eq
 |-  ( ( J e. Top /\ S C_ X ) -> { z e. ( Clsd ` J ) | S C_ z } = { z | E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) } )
44 43 inteqd
 |-  ( ( J e. Top /\ S C_ X ) -> |^| { z e. ( Clsd ` J ) | S C_ z } = |^| { z | E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) } )
45 difexg
 |-  ( X e. J -> ( X \ x ) e. _V )
46 45 ralrimivw
 |-  ( X e. J -> A. x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) e. _V )
47 dfiin2g
 |-  ( A. x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) e. _V -> |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) = |^| { z | E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) } )
48 7 46 47 3syl
 |-  ( J e. Top -> |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) = |^| { z | E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) } )
49 48 adantr
 |-  ( ( J e. Top /\ S C_ X ) -> |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) = |^| { z | E. x e. ( J i^i ~P ( X \ S ) ) z = ( X \ x ) } )
50 44 49 eqtr4d
 |-  ( ( J e. Top /\ S C_ X ) -> |^| { z e. ( Clsd ` J ) | S C_ z } = |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) )
51 1 clsval
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { z e. ( Clsd ` J ) | S C_ z } )
52 uniiun
 |-  U. ( J i^i ~P ( X \ S ) ) = U_ x e. ( J i^i ~P ( X \ S ) ) x
53 52 difeq2i
 |-  ( X \ U. ( J i^i ~P ( X \ S ) ) ) = ( X \ U_ x e. ( J i^i ~P ( X \ S ) ) x )
54 53 a1i
 |-  ( ( J e. Top /\ S C_ X ) -> ( X \ U. ( J i^i ~P ( X \ S ) ) ) = ( X \ U_ x e. ( J i^i ~P ( X \ S ) ) x ) )
55 0opn
 |-  ( J e. Top -> (/) e. J )
56 55 adantr
 |-  ( ( J e. Top /\ S C_ X ) -> (/) e. J )
57 0elpw
 |-  (/) e. ~P ( X \ S )
58 57 a1i
 |-  ( ( J e. Top /\ S C_ X ) -> (/) e. ~P ( X \ S ) )
59 56 58 elind
 |-  ( ( J e. Top /\ S C_ X ) -> (/) e. ( J i^i ~P ( X \ S ) ) )
60 ne0i
 |-  ( (/) e. ( J i^i ~P ( X \ S ) ) -> ( J i^i ~P ( X \ S ) ) =/= (/) )
61 iindif2
 |-  ( ( J i^i ~P ( X \ S ) ) =/= (/) -> |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) = ( X \ U_ x e. ( J i^i ~P ( X \ S ) ) x ) )
62 59 60 61 3syl
 |-  ( ( J e. Top /\ S C_ X ) -> |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) = ( X \ U_ x e. ( J i^i ~P ( X \ S ) ) x ) )
63 54 62 eqtr4d
 |-  ( ( J e. Top /\ S C_ X ) -> ( X \ U. ( J i^i ~P ( X \ S ) ) ) = |^|_ x e. ( J i^i ~P ( X \ S ) ) ( X \ x ) )
64 50 51 63 3eqtr4d
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( X \ U. ( J i^i ~P ( X \ S ) ) ) )
65 difssd
 |-  ( S C_ X -> ( X \ S ) C_ X )
66 1 ntrval
 |-  ( ( J e. Top /\ ( X \ S ) C_ X ) -> ( ( int ` J ) ` ( X \ S ) ) = U. ( J i^i ~P ( X \ S ) ) )
67 65 66 sylan2
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` ( X \ S ) ) = U. ( J i^i ~P ( X \ S ) ) )
68 67 difeq2d
 |-  ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( int ` J ) ` ( X \ S ) ) ) = ( X \ U. ( J i^i ~P ( X \ S ) ) ) )
69 64 68 eqtr4d
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( X \ ( ( int ` J ) ` ( X \ S ) ) ) )