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≠∅