Theorem bcth 7982

Description: Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, the metric space cannot be the countable union of rare closed subsets (where rare means having an empty interior), so some subset M` k 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.)

Hypotheses

Ref	Expression
bcth.1	|- X = dom dom D
bcth.2	|- J = (Open` D)

Assertion

Ref	Expression
bcth	|- (((D e. CMet /\ X =/= (/) /\ M:NN-->P~X) /\ (U.ran M = X /\ ran M (_ (Clsd` J))) -> E.k e. NN ((int` J)` (M` k)) =/= (/))

Distinct variable groups:   D,k   k,J   k,M   k,X

Proof of Theorem bcth

Step	Hyp	Ref	Expression
1		dmeq 3306	. . . . . . . . 9 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> dom D = dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
2	1	dmeqd 3308	. . . . . . . 8 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> dom dom D = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
3		bcth.1	. . . . . . . 8 |- X = dom dom D
4	2, 3	syl5eq 1516	. . . . . . 7 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> X = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
5		pweq 2399	. . . . . . 7 |- (X = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> P~X = P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
6	4, 5	syl 10	. . . . . 6 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> P~X = P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
7		feq3 3614	. . . . . 6 |- (P~X = P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (M:NN-->P~X <-> M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
8	6, 7	syl 10	. . . . 5 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (M:NN-->P~X <-> M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
9	4	eqeq2d 1483	. . . . . . 7 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (U.ran M = X <-> U.ran M = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
10		fveq2 3715	. . . . . . . . . 10 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (Open` D) = (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
11		bcth.2	. . . . . . . . . 10 |- J = (Open` D)
12	10, 11	syl5eq 1516	. . . . . . . . 9 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> J = (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
13	12	fveq2d 3719	. . . . . . . 8 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (Clsd` J) = (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - )))))
14	13	sseq2d 2085	. . . . . . 7 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (ran M (_ (Clsd` J) <-> ran M (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))))
15	9, 14	anbi12d 627	. . . . . 6 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> ((U.ran M = X /\ ran M (_ (Clsd` J)) <-> (U.ran M = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) /\ ran M (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - )))))))
16	12	fveq2d 3719	. . . . . . . . 9 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (int` J) = (int` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - )))))
17	16	fveq1d 3717	. . . . . . . 8 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> ((int` J)` (M` k)) = ((int` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))` (M` k)))
18	17	neeq1d 1591	. . . . . . 7 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (((int` J)` (M` k)) =/= (/) <-> ((int` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))` (M` k)) =/= (/)))
19	18	rexbidv 1661	. . . . . 6 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (E.k e. NN ((int` J)` (M` k)) =/= (/) <-> E.k e. NN ((int` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))` (M` k)) =/= (/)))
20	15, 19	imbi12d 625	. . . . 5 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> (((U.ran M = X /\ ran M (_ (Clsd` J)) -> E.k e. NN ((int` J)` (M` k)) =/= (/)) <-> ((U.ran M = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) /\ ran M (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))) -> E.k e. NN ((int` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))` (M` k)) =/= (/))))
21	8, 20	imbi12d 625	. . . 4 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> ((M:NN-->P~X -> ((U.ran M = X /\ ran M (_ (Clsd` J)) -> E.k e. NN ((int` J)` (M` k)) =/= (/))) <-> (M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> ((U.ran M = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) /\ ran M (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))) -> E.k e. NN ((int` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))` (M` k)) =/= (/)))))
22		rneq 3334	. . . . . . . . 9 |- (M = if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) -> ran M = ran if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})))
23	22	unieqd 2507	. . . . . . . 8 |- (M = if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) -> U.ran M = U.ran if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})))
24	23	eqeq1d 1480	. . . . . . 7 |- (M = if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) -> (U.ran M = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) <-> U.ran if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
25	22	sseq1d 2084	. . . . . . 7 |- (M = if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) -> (ran M (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - )))) <-> ran if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))))
26	24, 25	anbi12d 627	. . . . . 6 |- (M = if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) -> ((U.ran M = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) /\ ran M (_ (Clsd` (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))) <-> (U.ran if(M:NN-->P~dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )), M, (NN X. {(/)})) = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )) /\ ran