Theorem bcth 8032

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 3311	. . . . . . . . 9 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> dom D = dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
2	1	dmeqd 3313	. . . . . . . 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 1519	. . . . . . 7 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> X = dom dom if((D e. CMet /\ X =/= (/)), D, (abs o. - )))
5		pweq 2403	. . . . . . 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 3622	. . . . . 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 1486	. . . . . . 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 3724	. . . . . . . . . 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 1519	. . . . . . . . 9 |- (D = if((D e. CMet /\ X =/= (/)), D, (abs o. - )) -> J = (Open` if((D e. CMet /\ X =/= (/)), D, (abs o. - ))))
13	12	fveq2d 3728	. . . . . . . 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 2089	. . . . . . 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 628	. . . . . 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 3728	. . . . . . . . 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 3726	. . . . . . . 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 1594	. . . . . . 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 1664	. . . . . 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 626	. . . . 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 626	. . . 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 3339	. . . . . . . . 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 2512	. . . . . . . 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 1483	. . . . . . 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 2088	. . . . . . 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 628	. . . . . 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. - )) /\