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 ‘ 𝐽 ) ‘ 𝑐 ) ) )