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 = U. J
Assertion cldregopn 
|- ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A <-> E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) ) )

Proof

Step Hyp Ref Expression
1 opnregcld.1 
 |-  X = U. J
2 1 clscld 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` A ) e. ( 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 ) e. ( Clsd ` J ) /\ A = ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) ) -> E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) )
7 2 4 6 syl2an 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A ) -> E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) )
8 7 ex 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A -> E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) ) )
9 cldrcl 
 |-  ( c e. ( Clsd ` J ) -> J e. Top )
10 1 cldss 
 |-  ( c e. ( Clsd ` J ) -> c C_ X )
11 1 ntrss2 
 |-  ( ( J e. Top /\ c C_ X ) -> ( ( int ` J ) ` c ) C_ c )
12 9 10 11 syl2anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` c ) C_ c )
13 1 clsss2 
 |-  ( ( c e. ( Clsd ` J ) /\ ( ( int ` J ) ` c ) C_ c ) -> ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) C_ c )
14 12 13 mpdan 
 |-  ( c e. ( Clsd ` J ) -> ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) C_ c )
15 1 ntrss 
 |-  ( ( J e. Top /\ c C_ X /\ ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) C_ c ) -> ( ( int ` J ) ` ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) C_ ( ( int ` J ) ` c ) )
16 9 10 14 15 syl3anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) C_ ( ( int ` J ) ` c ) )
17 1 ntridm 
 |-  ( ( J e. Top /\ c C_ X ) -> ( ( int ` J ) ` ( ( int ` J ) ` c ) ) = ( ( int ` J ) ` c ) )
18 9 10 17 syl2anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` ( ( int ` J ) ` c ) ) = ( ( int ` J ) ` c ) )
19 1 ntrss3 
 |-  ( ( J e. Top /\ c C_ X ) -> ( ( int ` J ) ` c ) C_ X )
20 9 10 19 syl2anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` c ) C_ X )
21 1 clsss3 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` c ) C_ X ) -> ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) C_ X )
22 9 20 21 syl2anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) C_ X )
23 1 sscls 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` c ) C_ X ) -> ( ( int ` J ) ` c ) C_ ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) )
24 9 20 23 syl2anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` c ) C_ ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) )
25 1 ntrss 
 |-  ( ( J e. Top /\ ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) C_ X /\ ( ( int ` J ) ` c ) C_ ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) -> ( ( int ` J ) ` ( ( int ` J ) ` c ) ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) )
26 9 22 24 25 syl3anc 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` ( ( int ` J ) ` c ) ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) )
27 18 26 eqsstrrd 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` c ) C_ ( ( int ` J ) ` ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) )
28 16 27 eqssd 
 |-  ( c e. ( Clsd ` J ) -> ( ( int ` J ) ` ( ( cls ` J ) ` ( ( int ` J ) ` c ) ) ) = ( ( int ` J ) ` c ) )
29 28 adantl 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ c e. ( 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 e. Top /\ A C_ X ) /\ c e. ( Clsd ` J ) ) -> ( A = ( ( int ` J ) ` c ) -> ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A ) )
34 33 rexlimdva 
 |-  ( ( J e. Top /\ A C_ X ) -> ( E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) -> ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A ) )
35 8 34 impbid 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A <-> E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) ) )