This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmclsopn

Description: The complement of a closure is open. (Contributed by NM, 11-Sep-2006)

Ref Expression
Hypothesis clscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cmclsopn ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 clsval2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )
3 2 difeq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) )
4 difss ⊢ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋
5 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ∈ 𝐽 )
6 4 5 mpan2 ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ∈ 𝐽 )
7 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ 𝑋 )
8 6 7 mpdan ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ 𝑋 )
9 dfss4 ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) )
10 8 9 sylib ⊢ ( 𝐽 ∈ Top → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) )
11 10 6 eqeltrd ⊢ ( 𝐽 ∈ Top → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) ∈ 𝐽 )
12 11 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) ) ∈ 𝐽 )
13 3 12 eqeltrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )