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 syl5eq ( 𝑘 = 𝑛 → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝑋𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 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 simpr ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ) → ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ )
32 16 fveqeq2d ( 𝑘 = 𝑛 → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ↔ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑛 ) ) = ∅ ) )
33 32 cbvralvw ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ↔ ∀ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑛 ) ) = ∅ )
34 31 33 sylib ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ) → ∀ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑛 ) ) = ∅ )
35 1 2 29 30 34 bcthlem5 ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) ∧ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ) → ( ( int ‘ 𝐽 ) ‘ ran 𝑀 ) = ∅ )
36 35 ex ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ → ( ( int ‘ 𝐽 ) ‘ ran 𝑀 ) = ∅ ) )
37 36 necon3ad ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ( ( int ‘ 𝐽 ) ‘ ran 𝑀 ) ≠ ∅ → ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ) )
38 37 3impia ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ ran 𝑀 ) ≠ ∅ ) → ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ )
39 df-ne ( ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) ≠ ∅ ↔ ¬ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ )
40 39 rexbii ( ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) ≠ ∅ ↔ ∃ 𝑘 ∈ ℕ ¬ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ )
41 rexnal ( ∃ 𝑘 ∈ ℕ ¬ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ ↔ ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ )
42 40 41 bitri ( ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) ≠ ∅ ↔ ¬ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) = ∅ )
43 38 42 sylibr ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ ran 𝑀 ) ≠ ∅ ) → ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀𝑘 ) ) ≠ ∅ )