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

Metamath Proof Explorer

Theorem 0ntr

Description: A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006)

Ref Expression
Hypothesis clscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion 0ntr ( ( ( 𝐽 ∈ Top ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) → ( 𝑋 ∖ 𝑆 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 ssdif0 ⊢ ( 𝑋 ⊆ 𝑆 ↔ ( 𝑋 ∖ 𝑆 ) = ∅ )
3 eqss ⊢ ( 𝑆 = 𝑋 ↔ ( 𝑆 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) )
4 fveq2 ⊢ ( 𝑆 = 𝑋 → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( ( int ‘ 𝐽 ) ‘ 𝑋 ) )
5 1 ntrtop ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )
6 4 5 sylan9eqr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑋 )
7 6 eqeq1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ↔ 𝑋 = ∅ ) )
8 7 biimpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 = 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ → 𝑋 = ∅ ) )
9 8 ex ⊢ ( 𝐽 ∈ Top → ( 𝑆 = 𝑋 → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ → 𝑋 = ∅ ) ) )
10 3 9 biimtrrid ⊢ ( 𝐽 ∈ Top → ( ( 𝑆 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑆 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ → 𝑋 = ∅ ) ) )
11 10 expd ⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 → ( 𝑋 ⊆ 𝑆 → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ → 𝑋 = ∅ ) ) ) )
12 11 com34 ⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ → ( 𝑋 ⊆ 𝑆 → 𝑋 = ∅ ) ) ) )
13 12 imp32 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) → ( 𝑋 ⊆ 𝑆 → 𝑋 = ∅ ) )
14 2 13 biimtrrid ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) → ( ( 𝑋 ∖ 𝑆 ) = ∅ → 𝑋 = ∅ ) )
15 14 necon3d ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) → ( 𝑋 ≠ ∅ → ( 𝑋 ∖ 𝑆 ) ≠ ∅ ) )
16 15 imp ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ∖ 𝑆 ) ≠ ∅ )
17 16 an32s ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑆 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) → ( 𝑋 ∖ 𝑆 ) ≠ ∅ )