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 ⊢ X = ⋃ J
Assertion 0ntr ⊢ J ∈ Top ∧ X ≠ ∅ ∧ S ⊆ X ∧ int ⁡ J ⁡ S = ∅ → X ∖ S ≠ ∅

Proof

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