Metamath Proof Explorer

Theorem bcth

Description: Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having a closure with empty interior), so some subset Mk must have a nonempty interior. Theorem 4.7-2 of Kreyszig p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 for an overview of the proof. (Contributed by NM, 28-Oct-2007) (Proof shortened by Mario Carneiro, 6-Jan-2014)

Ref Expression
Hypothesis bcth.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion bcth ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ≠ ∅ ) → ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 bcth.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 simpll ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋 ) )
4 eleq1w ⊢ ( 𝑟 = 𝑚 → ( 𝑟 ∈ ℝ+ ↔ 𝑚 ∈ ℝ+ ) )
5 3 4 bi2anan9 ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ) )
6 simpr ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → 𝑟 = 𝑚 )
7 6 breq1d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( 𝑟 < ( 1 / 𝑘 ) ↔ 𝑚 < ( 1 / 𝑘 ) ) )
8 oveq12 ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) )
9 8 fveq2d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) )
10 9 sseq1d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) )
11 7 10 anbi12d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ↔ ( 𝑚 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) )
12 5 11 anbi12d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑟 = 𝑚 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) )
13 12 cbvopabv ⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } = { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) }
14 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 1 / 𝑘 ) = ( 1 / 𝑛 ) )
15 14 breq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑚 < ( 1 / 𝑘 ) ↔ 𝑚 < ( 1 / 𝑛 ) ) )
16 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑀 ‘ 𝑘 ) = ( 𝑀 ‘ 𝑛 ) )
17 16 difeq2d ⊢ ( 𝑘 = 𝑛 → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) = ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) )
18 17 sseq2d ⊢ ( 𝑘 = 𝑛 → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) )
19 15 18 anbi12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑚 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ↔ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) )
20 19 anbi2d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) ) )
21 20 opabbidv ⊢ ( 𝑘 = 𝑛 → { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } = { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) } )
22 13 21 eqtrid ⊢ ( 𝑘 = 𝑛 → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } = { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) } )
23 fveq2 ⊢ ( 𝑧 = 𝑔 → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) = ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) )
24 23 difeq1d ⊢ ( 𝑧 = 𝑔 → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) = ( ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) ∖ ( 𝑀 ‘ 𝑛 ) ) )
25 24 sseq2d ⊢ ( 𝑧 = 𝑔 → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) )
26 25 anbi2d ⊢ ( 𝑧 = 𝑔 → ( ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ↔ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) )
27 26 anbi2d ⊢ ( 𝑧 = 𝑔 → ( ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) ↔ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) ) )
28 27 opabbidv ⊢ ( 𝑧 = 𝑔 → { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) } = { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) } )
29 22 28 cbvmpov ⊢ ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ+ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ) = ( 𝑛 ∈ ℕ , 𝑔 ∈ ( 𝑋 × ℝ+ ) ↦ { ⟨ 𝑦 , 𝑚 ⟩ ∣ ( ( 𝑦 ∈ 𝑋 ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑚 < ( 1 / 𝑛 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑦 ( ball ‘ 𝐷 ) 𝑚 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑔 ) ∖ ( 𝑀 ‘ 𝑛 ) ) ) ) } )
30 simplr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
31 16 fveqeq2d ⊢ ( 𝑘 = 𝑛 → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ↔ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑛 ) ) = ∅ ) )
32 31 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ↔ ∀ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑛 ) ) = ∅ )
33 32 bilani ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) → ∀ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑛 ) ) = ∅ )
34 1 2 29 30 33 bcthlem5 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) = ∅ )
35 34 ex ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) = ∅ ) )
36 35 necon3ad ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ≠ ∅ → ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) )
37 36 3impia ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ≠ ∅ ) → ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ )
38 df-ne ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ↔ ¬ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ )
39 38 rexbii ⊢ ( ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ↔ ∃ 𝑘 ∈ ℕ ¬ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ )
40 rexnal ⊢ ( ∃ 𝑘 ∈ ℕ ¬ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ↔ ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ )
41 39 40 bitri ⊢ ( ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ↔ ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ )
42 37 41 sylibr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ≠ ∅ ) → ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ )