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 ⊢ 𝑋 = ∪ 𝐽
Assertion opnregcld ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ↔ ∃ 𝑜 ∈ 𝐽 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )

Proof

Step Hyp Ref Expression
1 opnregcld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 )
3 eqcom ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ↔ 𝐴 = ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
4 3 biimpi ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 → 𝐴 = ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
5 fveq2 ⊢ ( 𝑜 = ( ( int ‘ 𝐽 ) ‘ 𝐴 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) = ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
6 5 rspceeqv ⊢ ( ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 ∧ 𝐴 = ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ∃ 𝑜 ∈ 𝐽 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
7 2 4 6 syl2an ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ) → ∃ 𝑜 ∈ 𝐽 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
8 7 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 → ∃ 𝑜 ∈ 𝐽 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )
9 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝐽 ∈ Top )
10 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ 𝑋 )
11 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑋 )
12 10 11 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑋 )
13 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
14 12 13 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
15 1 clsss ⊢ ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )
16 9 12 14 15 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )
17 1 clsidm ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
18 10 17 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
19 16 18 sseqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
20 1 ntrss3 ⊢ ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ⊆ 𝑋 )
21 12 20 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ⊆ 𝑋 )
22 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ∈ 𝐽 )
23 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋 ) → 𝑜 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
24 10 23 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
25 1 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) → 𝑜 ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )
26 9 12 22 24 25 syl22anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )
27 1 clsss ⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ⊆ 𝑋 ∧ 𝑜 ⊆ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) )
28 9 21 26 27 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) )
29 19 28 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
30 29 adantlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
31 2fveq3 ⊢ ( 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) )
32 id ⊢ ( 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) → 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
33 31 32 eqeq12d ⊢ ( 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ↔ ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )
34 30 33 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ) )
35 34 rexlimdva ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ∃ 𝑜 ∈ 𝐽 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ) )
36 8 35 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = 𝐴 ↔ ∃ 𝑜 ∈ 𝐽 𝐴 = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ) )