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 ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ) ) → ( 𝑋 ∖ 𝑆 ) ≠ ∅ )