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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion bcth2 ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ∪ ran 𝑀 = 𝑋 ) ) → ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ )

Proof

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