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