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 𝑋 = 𝐽
Assertion cldregopn ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ↔ ∃ 𝑐 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( ( int ‘ 𝐽 ) ‘ 𝑐 ) ) )

Proof

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