Metamath Proof Explorer

Theorem opnregcld

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

Ref Expression
Hypothesis opnregcld.1 
|- X = U. J
Assertion opnregcld 
|- ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A <-> E. o e. J A = ( ( cls ` J ) ` o ) ) )

Proof

Step Hyp Ref Expression
1 opnregcld.1 
 |-  X = U. J
2 1 ntropn 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) e. J )
3 eqcom 
 |-  ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A <-> A = ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) )
4 3 biimpi 
 |-  ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A -> A = ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) )
5 fveq2 
 |-  ( o = ( ( int ` J ) ` A ) -> ( ( cls ` J ) ` o ) = ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) )
6 5 rspceeqv 
 |-  ( ( ( ( int ` J ) ` A ) e. J /\ A = ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) ) -> E. o e. J A = ( ( cls ` J ) ` o ) )
7 2 4 6 syl2an 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A ) -> E. o e. J A = ( ( cls ` J ) ` o ) )
8 7 ex 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A -> E. o e. J A = ( ( cls ` J ) ` o ) ) )
9 simpl 
 |-  ( ( J e. Top /\ o e. J ) -> J e. Top )
10 1 eltopss 
 |-  ( ( J e. Top /\ o e. J ) -> o C_ X )
11 1 clsss3 
 |-  ( ( J e. Top /\ o C_ X ) -> ( ( cls ` J ) ` o ) C_ X )
12 10 11 syldan 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( cls ` J ) ` o ) C_ X )
13 1 ntrss2 
 |-  ( ( J e. Top /\ ( ( cls ` J ) ` o ) C_ X ) -> ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) C_ ( ( cls ` J ) ` o ) )
14 12 13 syldan 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) C_ ( ( cls ` J ) ` o ) )
15 1 clsss 
 |-  ( ( J e. Top /\ ( ( cls ` J ) ` o ) C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) C_ ( ( cls ` J ) ` o ) ) -> ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) C_ ( ( cls ` J ) ` ( ( cls ` J ) ` o ) ) )
16 9 12 14 15 syl3anc 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) C_ ( ( cls ` J ) ` ( ( cls ` J ) ` o ) ) )
17 1 clsidm 
 |-  ( ( J e. Top /\ o C_ X ) -> ( ( cls ` J ) ` ( ( cls ` J ) ` o ) ) = ( ( cls ` J ) ` o ) )
18 10 17 syldan 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( cls ` J ) ` ( ( cls ` J ) ` o ) ) = ( ( cls ` J ) ` o ) )
19 16 18 sseqtrd 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) C_ ( ( cls ` J ) ` o ) )
20 1 ntrss3 
 |-  ( ( J e. Top /\ ( ( cls ` J ) ` o ) C_ X ) -> ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) C_ X )
21 12 20 syldan 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) C_ X )
22 simpr 
 |-  ( ( J e. Top /\ o e. J ) -> o e. J )
23 1 sscls 
 |-  ( ( J e. Top /\ o C_ X ) -> o C_ ( ( cls ` J ) ` o ) )
24 10 23 syldan 
 |-  ( ( J e. Top /\ o e. J ) -> o C_ ( ( cls ` J ) ` o ) )
25 1 ssntr 
 |-  ( ( ( J e. Top /\ ( ( cls ` J ) ` o ) C_ X ) /\ ( o e. J /\ o C_ ( ( cls ` J ) ` o ) ) ) -> o C_ ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) )
26 9 12 22 24 25 syl22anc 
 |-  ( ( J e. Top /\ o e. J ) -> o C_ ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) )
27 1 clsss 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) C_ X /\ o C_ ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) -> ( ( cls ` J ) ` o ) C_ ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) )
28 9 21 26 27 syl3anc 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( cls ` J ) ` o ) C_ ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) )
29 19 28 eqssd 
 |-  ( ( J e. Top /\ o e. J ) -> ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) = ( ( cls ` J ) ` o ) )
30 29 adantlr 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ o e. J ) -> ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) = ( ( cls ` J ) ` o ) )
31 2fveq3 
 |-  ( A = ( ( cls ` J ) ` o ) -> ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) )
32 id 
 |-  ( A = ( ( cls ` J ) ` o ) -> A = ( ( cls ` J ) ` o ) )
33 31 32 eqeq12d 
 |-  ( A = ( ( cls ` J ) ` o ) -> ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A <-> ( ( cls ` J ) ` ( ( int ` J ) ` ( ( cls ` J ) ` o ) ) ) = ( ( cls ` J ) ` o ) ) )
34 30 33 syl5ibrcom 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ o e. J ) -> ( A = ( ( cls ` J ) ` o ) -> ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A ) )
35 34 rexlimdva 
 |-  ( ( J e. Top /\ A C_ X ) -> ( E. o e. J A = ( ( cls ` J ) ` o ) -> ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A ) )
36 8 35 impbid 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A <-> E. o e. J A = ( ( cls ` J ) ` o ) ) )