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	$⊢ J = MetOpen (D)$
	Assertion	bcth	$⊢ (D \in CMet (X) \land M : ℕ ⟶ Clsd (J) \land int (J) (⋃ ran M) \neq \emptyset) \to \exists k \in ℕ int (J) (M (k)) \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		bcth.2	$⊢ J = MetOpen (D)$
2		simpll	$⊢ ((D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \land \forall k \in ℕ int (J) (M (k)) = \emptyset) \to D \in CMet (X)$
3		eleq1w	$⊢ x = y \to (x \in X \leftrightarrow y \in X)$
4		eleq1w	$⊢ r = m \to (r \in ℝ^{+} \leftrightarrow m \in ℝ^{+})$
5	3 4	bi2anan9	$⊢ (x = y \land r = m) \to ((x \in X \land r \in ℝ^{+}) \leftrightarrow (y \in X \land m \in ℝ^{+}))$
6		simpr	$⊢ (x = y \land r = m) \to r = m$
7	6	breq1d	$⊢ (x = y \land r = m) \to (r < \frac{1}{k} \leftrightarrow m < \frac{1}{k})$
8		oveq12	$⊢ (x = y \land r = m) \to x ball (D) r = y ball (D) m$
9	8	fveq2d	$⊢ (x = y \land r = m) \to cls (J) (x ball (D) r) = cls (J) (y ball (D) m)$
10	9	sseq1d	$⊢ (x = y \land r = m) \to (cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k) \leftrightarrow cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k))$
11	7 10	anbi12d	$⊢ (x = y \land r = m) \to ((r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)) \leftrightarrow (m < \frac{1}{k} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k)))$
12	5 11	anbi12d	$⊢ (x = y \land r = m) \to (((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k))) \leftrightarrow ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{k} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k))))$
13	12	cbvopabv	$⊢ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\} = \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{k} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k)))\}$
14		oveq2	$⊢ k = n \to \frac{1}{k} = \frac{1}{n}$
15	14	breq2d	$⊢ k = n \to (m < \frac{1}{k} \leftrightarrow m < \frac{1}{n})$
16		fveq2	$⊢ k = n \to M (k) = M (n)$
17	16	difeq2d	$⊢ k = n \to ball (D) (z) ∖ M (k) = ball (D) (z) ∖ M (n)$
18	17	sseq2d	$⊢ k = n \to (cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k) \leftrightarrow cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n))$
19	15 18	anbi12d	$⊢ k = n \to ((m < \frac{1}{k} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k)) \leftrightarrow (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n)))$
20	19	anbi2d	$⊢ k = n \to (((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{k} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k))) \leftrightarrow ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n))))$
21	20	opabbidv	$⊢ k = n \to \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{k} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (k)))\} = \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n)))\}$
22	13 21	syl5eq	$⊢ k = n \to \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\} = \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n)))\}$
23		fveq2	$⊢ z = g \to ball (D) (z) = ball (D) (g)$
24	23	difeq1d	$⊢ z = g \to ball (D) (z) ∖ M (n) = ball (D) (g) ∖ M (n)$
25	24	sseq2d	$⊢ z = g \to (cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n) \leftrightarrow cls (J) (y ball (D) m) \subseteq ball (D) (g) ∖ M (n))$
26	25	anbi2d	$⊢ z = g \to ((m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n)) \leftrightarrow (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (g) ∖ M (n)))$
27	26	anbi2d	$⊢ z = g \to (((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n))) \leftrightarrow ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (g) ∖ M (n))))$
28	27	opabbidv	$⊢ z = g \to \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (z) ∖ M (n)))\} = \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (g) ∖ M (n)))\}$
29	22 28	cbvmpov	$⊢ (k \in ℕ, z \in (X \times ℝ^{+}) ⟼ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\}) = (n \in ℕ, g \in (X \times ℝ^{+}) ⟼ \{⟨y, m⟩ \| ((y \in X \land m \in ℝ^{+}) \land (m < \frac{1}{n} \land cls (J) (y ball (D) m) \subseteq ball (D) (g) ∖ M (n)))\})$
30		simplr	$⊢ ((D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \land \forall k \in ℕ int (J) (M (k)) = \emptyset) \to M : ℕ ⟶ Clsd (J)$
31		simpr	$⊢ ((D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \land \forall k \in ℕ int (J) (M (k)) = \emptyset) \to \forall k \in ℕ int (J) (M (k)) = \emptyset$
32	16	fveqeq2d	$⊢ k = n \to (int (J) (M (k)) = \emptyset \leftrightarrow int (J) (M (n)) = \emptyset)$
33	32	cbvralvw	$⊢ \forall k \in ℕ int (J) (M (k)) = \emptyset \leftrightarrow \forall n \in ℕ int (J) (M (n)) = \emptyset$
34	31 33	sylib	$⊢ ((D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \land \forall k \in ℕ int (J) (M (k)) = \emptyset) \to \forall n \in ℕ int (J) (M (n)) = \emptyset$
35	1 2 29 30 34	bcthlem5	$⊢ ((D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \land \forall k \in ℕ int (J) (M (k)) = \emptyset) \to int (J) (⋃ ran M) = \emptyset$
36	35	ex	$⊢ (D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \to (\forall k \in ℕ int (J) (M (k)) = \emptyset \to int (J) (⋃ ran M) = \emptyset)$
37	36	necon3ad	$⊢ (D \in CMet (X) \land M : ℕ ⟶ Clsd (J)) \to (int (J) (⋃ ran M) \neq \emptyset \to \neg \forall k \in ℕ int (J) (M (k)) = \emptyset)$
38	37	3impia	$⊢ (D \in CMet (X) \land M : ℕ ⟶ Clsd (J) \land int (J) (⋃ ran M) \neq \emptyset) \to \neg \forall k \in ℕ int (J) (M (k)) = \emptyset$
39		df-ne	$⊢ int (J) (M (k)) \neq \emptyset \leftrightarrow \neg int (J) (M (k)) = \emptyset$
40	39	rexbii	$⊢ \exists k \in ℕ int (J) (M (k)) \neq \emptyset \leftrightarrow \exists k \in ℕ \neg int (J) (M (k)) = \emptyset$
41		rexnal	$⊢ \exists k \in ℕ \neg int (J) (M (k)) = \emptyset \leftrightarrow \neg \forall k \in ℕ int (J) (M (k)) = \emptyset$
42	40 41	bitri	$⊢ \exists k \in ℕ int (J) (M (k)) \neq \emptyset \leftrightarrow \neg \forall k \in ℕ int (J) (M (k)) = \emptyset$
43	38 42	sylibr	$⊢ (D \in CMet (X) \land M : ℕ ⟶ Clsd (J) \land int (J) (⋃ ran M) \neq \emptyset) \to \exists k \in ℕ int (J) (M (k)) \neq \emptyset$

Metamath Proof Explorer

Theorem bcth

Proof