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

Metamath Proof Explorer

Theorem ntreq0

Description: Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis clscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion ntreq0 ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑥 ⊆ 𝑆 → 𝑥 = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 ntrval ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
3 2 eqeq1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ↔ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = ∅ ) )
4 neq0 ⊢ ( ¬ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = ∅ ↔ ∃ 𝑦 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
5 4 con1bii ⊢ ( ¬ ∃ 𝑦 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = ∅ )
6 ancom ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ) ↔ ( 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑥 ) )
7 elin ⊢ ( 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ∈ 𝒫 𝑆 ) )
8 7 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑥 ) )
9 anass ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ) )
10 6 8 9 3bitri ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ) ↔ ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ) )
11 10 exbii ⊢ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ) )
12 eluni ⊢ ( 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ) )
13 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ) )
14 11 12 13 3bitr4i ⊢ ( 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) )
15 14 exbii ⊢ ( ∃ 𝑦 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) )
16 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) )
17 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝒫 𝑆 ∧ ∃ 𝑦 𝑦 ∈ 𝑥 ) )
18 17 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ ∃ 𝑦 𝑦 ∈ 𝑥 ) )
19 15 16 18 3bitr2i ⊢ ( ∃ 𝑦 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ ∃ 𝑦 𝑦 ∈ 𝑥 ) )
20 19 notbii ⊢ ( ¬ ∃ 𝑦 𝑦 ∈ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ¬ ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ ∃ 𝑦 𝑦 ∈ 𝑥 ) )
21 5 20 bitr3i ⊢ ( ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = ∅ ↔ ¬ ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ ∃ 𝑦 𝑦 ∈ 𝑥 ) )
22 ralinexa ⊢ ( ∀ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 → ¬ ∃ 𝑦 𝑦 ∈ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 ∧ ∃ 𝑦 𝑦 ∈ 𝑥 ) )
23 velpw ⊢ ( 𝑥 ∈ 𝒫 𝑆 ↔ 𝑥 ⊆ 𝑆 )
24 neq0 ⊢ ( ¬ 𝑥 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
25 24 con1bii ⊢ ( ¬ ∃ 𝑦 𝑦 ∈ 𝑥 ↔ 𝑥 = ∅ )
26 23 25 imbi12i ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 → ¬ ∃ 𝑦 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ⊆ 𝑆 → 𝑥 = ∅ ) )
27 26 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐽 ( 𝑥 ∈ 𝒫 𝑆 → ¬ ∃ 𝑦 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑥 ⊆ 𝑆 → 𝑥 = ∅ ) )
28 21 22 27 3bitr2i ⊢ ( ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑥 ⊆ 𝑆 → 𝑥 = ∅ ) )
29 3 28 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑥 ⊆ 𝑆 → 𝑥 = ∅ ) ) )