Metamath Proof Explorer

Theorem bcth2

Description: Baire's Category Theorem, version 2: If countably many closed sets cover X , then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014)

Ref Expression
Hypothesis bcth.2 ⊢ J = MetOpen ⁡ D
Assertion bcth2 ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → ∃ k ∈ ℕ int ⁡ J ⁡ M ⁡ k ≠ ∅

Proof

Step Hyp Ref Expression
1 bcth.2 ⊢ J = MetOpen ⁡ D
2 simpll ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → D ∈ CMet ⁡ X
3 simprl ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → M : ℕ ⟶ Clsd ⁡ J
4 cmetmet ⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X
5 4 ad2antrr ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → D ∈ Met ⁡ X
6 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
7 1 mopntopon ⊢ D ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X
8 5 6 7 3syl ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → J ∈ TopOn ⁡ X
9 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
10 8 9 syl ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → J ∈ Top
11 simprr ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → ⋃ ran ⁡ M = X
12 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
13 8 12 syl ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → X ∈ J
14 11 13 eqeltrd ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → ⋃ ran ⁡ M ∈ J
15 isopn3i ⊢ J ∈ Top ∧ ⋃ ran ⁡ M ∈ J → int ⁡ J ⁡ ⋃ ran ⁡ M = ⋃ ran ⁡ M
16 10 14 15 syl2anc ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → int ⁡ J ⁡ ⋃ ran ⁡ M = ⋃ ran ⁡ M
17 16 11 eqtrd ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → int ⁡ J ⁡ ⋃ ran ⁡ M = X
18 simplr ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → X ≠ ∅
19 17 18 eqnetrd ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → int ⁡ J ⁡ ⋃ ran ⁡ M ≠ ∅
20 1 bcth ⊢ D ∈ CMet ⁡ X ∧ M : ℕ ⟶ Clsd ⁡ J ∧ int ⁡ J ⁡ ⋃ ran ⁡ M ≠ ∅ → ∃ k ∈ ℕ int ⁡ J ⁡ M ⁡ k ≠ ∅
21 2 3 19 20 syl3anc ⊢ D ∈ CMet ⁡ X ∧ X ≠ ∅ ∧ M : ℕ ⟶ Clsd ⁡ J ∧ ⋃ ran ⁡ M = X → ∃ k ∈ ℕ int ⁡ J ⁡ M ⁡ k ≠ ∅