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⁡JA=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⁡JA=int⁡J⁡c
7 2 4 6 syl2an ⊢J∈Top∧A⊆X∧int⁡J⁡cls⁡J⁡A=A→∃c∈Clsd⁡JA=int⁡J⁡c
8 7 ex ⊢J∈Top∧A⊆X→int⁡J⁡cls⁡J⁡A=A→∃c∈Clsd⁡JA=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⁡JA=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⁡JA=int⁡J⁡c