Theorem bcth 25560

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 𝑀‘𝑘 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 25559 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.)

Hypothesis

Ref	Expression
bcth.2	⊢ 𝐽 = (MetOpen‘𝐷)

Assertion

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

Distinct variable groups:   𝐷,𝑘   𝑘,𝐽   𝑘,𝑀   𝑘,𝑋

Proof of Theorem bcth

Dummy variables 𝑛 𝑟 𝑥 𝑧 𝑔 𝑚 𝑦 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  ∃wrex 3086   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4279  ∪ cuni 4867   class class class wbr 5103  {copab 5167   × cxp 5653  ran crn 5656  ⟶wf 6529  ‘cfv 6533  (class class class)co 7414   ∈ cmpo 7416  1c1 11128   < clt 11270   / cdiv 11898  ℕcn 12260  ℝ⁺crp 13045  ballcbl 21575  MetOpencmopn 21578  Clsdccld 23244  intcnt 23245  clsccl 23246  CMetccmet 25485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-inf2 9623  ax-dc 10451  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8458  df-er 8699  df-map 8831  df-pm 8832  df-en 8956  df-dom 8957  df-sdom 8958  df-sup 9415  df-inf 9416  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-n0 12532  df-z 12619  df-uz 12891  df-q 13001  df-rp 13046  df-xneg 13166  df-xadd 13167  df-xmul 13168  df-ico 13407  df-rest 17510  df-topgen 17531  df-psmet 21580  df-xmet 21581  df-met 21582  df-bl 21583  df-mopn 21584  df-fbas 21585  df-fg 21586  df-top 23122  df-topon 23139  df-bases 23174  df-cld 23247  df-ntr 23248  df-cls 23249  df-nei 23326  df-lm 23457  df-fil 24075  df-fm 24167  df-flim 24168  df-flf 24169  df-cfil 25486  df-cau 25487  df-cmet 25488

This theorem is used by:  bcth2  25561  bcth3  25562