Metamath Proof Explorer


Theorem cldregopn

Description: A set if regularly open iff it is the interior of some closed set. (Contributed by Jeff Hankins, 27-Sep-2009)

Ref Expression
Hypothesis opnregcld.1 X = J
Assertion cldregopn J Top A X int J cls J A = A c Clsd J A = int J c

Proof

Step Hyp Ref Expression
1 opnregcld.1 X = J
2 1 clscld J Top A X cls J A Clsd J
3 eqcom int J cls J A = A A = int J cls J A
4 3 biimpi int J cls J A = A A = int J cls J A
5 fveq2 c = cls J A int J c = int J cls J A
6 5 rspceeqv cls J A Clsd J A = int J cls J A c Clsd J A = int J c
7 2 4 6 syl2an J Top A X int J cls J A = A c Clsd J A = int J c
8 7 ex J Top A X int J cls J A = A c Clsd J A = int J c
9 cldrcl c Clsd J J Top
10 1 cldss c Clsd J c X
11 1 ntrss2 J Top c X int J c c
12 9 10 11 syl2anc c Clsd J int J c c
13 1 clsss2 c Clsd J int J c c cls J int J c c
14 12 13 mpdan c Clsd J cls J int J c c
15 1 ntrss J Top c X cls J int J c c int J cls J int J c int J c
16 9 10 14 15 syl3anc c Clsd J int J cls J int J c int J c
17 1 ntridm J Top c X int J int J c = int J c
18 9 10 17 syl2anc c Clsd J int J int J c = int J c
19 1 ntrss3 J Top c X int J c X
20 9 10 19 syl2anc c Clsd J int J c X
21 1 clsss3 J Top int J c X cls J int J c X
22 9 20 21 syl2anc c Clsd J cls J int J c X
23 1 sscls J Top int J c X int J c cls J int J c
24 9 20 23 syl2anc c Clsd J int J c cls J int J c
25 1 ntrss J Top cls J int J c X int J c cls J int J c int J int J c int J cls J int J c
26 9 22 24 25 syl3anc c Clsd J int J int J c int J cls J int J c
27 18 26 eqsstrrd c Clsd J int J c int J cls J int J c
28 16 27 eqssd c Clsd J int J cls J int J c = int J c
29 28 adantl J Top A X c Clsd J int J cls J int J c = int J c
30 2fveq3 A = int J c int J cls J A = int J cls J int J c
31 id A = int J c A = int J c
32 30 31 eqeq12d A = int J c int J cls J A = A int J cls J int J c = int J c
33 29 32 syl5ibrcom J Top A X c Clsd J A = int J c int J cls J A = A
34 33 rexlimdva J Top A X c Clsd J A = int J c int J cls J A = A
35 8 34 impbid J Top A X int J cls J A = A c Clsd J A = int J c