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