Metamath Proof Explorer


Theorem heibor1

Description: One half of heibor , that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet and total boundedness here, which follows trivially from the fact that the set of all r -balls is an open cover of X , so finitely many cover X . (Contributed by Jeff Madsen, 16-Jan-2014)

Ref Expression
Hypothesis heibor.1 J = MetOpen D
Assertion heibor1 D Met X J Comp D CMet X D TotBnd X

Proof

Step Hyp Ref Expression
1 heibor.1 J = MetOpen D
2 simpll D Met X J Comp x Cau D x : X D Met X
3 simplr D Met X J Comp x Cau D x : X J Comp
4 simprl D Met X J Comp x Cau D x : X x Cau D
5 simprr D Met X J Comp x Cau D x : X x : X
6 1 2 3 4 5 heibor1lem D Met X J Comp x Cau D x : X x dom t J
7 6 expr D Met X J Comp x Cau D x : X x dom t J
8 7 ralrimiva D Met X J Comp x Cau D x : X x dom t J
9 nnuz = 1
10 1zzd D Met X J Comp 1
11 simpl D Met X J Comp D Met X
12 9 1 10 11 iscmet3 D Met X J Comp D CMet X x Cau D x : X x dom t J
13 8 12 mpbird D Met X J Comp D CMet X
14 simplr D Met X J Comp r + J Comp
15 metxmet D Met X D ∞Met X
16 id z X z X
17 rpxr r + r *
18 1 blopn D ∞Met X z X r * z ball D r J
19 15 16 17 18 syl3an D Met X z X r + z ball D r J
20 19 3com23 D Met X r + z X z ball D r J
21 20 3expa D Met X r + z X z ball D r J
22 eleq1a z ball D r J y = z ball D r y J
23 21 22 syl D Met X r + z X y = z ball D r y J
24 23 rexlimdva D Met X r + z X y = z ball D r y J
25 24 adantlr D Met X J Comp r + z X y = z ball D r y J
26 25 abssdv D Met X J Comp r + y | z X y = z ball D r J
27 15 ad2antrr D Met X J Comp r + D ∞Met X
28 1 mopnuni D ∞Met X X = J
29 27 28 syl D Met X J Comp r + X = J
30 blcntr D ∞Met X z X r + z z ball D r
31 15 30 syl3an1 D Met X z X r + z z ball D r
32 31 3com23 D Met X r + z X z z ball D r
33 32 3expa D Met X r + z X z z ball D r
34 ovex z ball D r V
35 34 elabrex z X z ball D r y | z X y = z ball D r
36 35 adantl D Met X r + z X z ball D r y | z X y = z ball D r
37 elunii z z ball D r z ball D r y | z X y = z ball D r z y | z X y = z ball D r
38 33 36 37 syl2anc D Met X r + z X z y | z X y = z ball D r
39 38 ralrimiva D Met X r + z X z y | z X y = z ball D r
40 39 adantlr D Met X J Comp r + z X z y | z X y = z ball D r
41 nfcv _ z X
42 nfre1 z z X y = z ball D r
43 42 nfab _ z y | z X y = z ball D r
44 43 nfuni _ z y | z X y = z ball D r
45 41 44 dfss3f X y | z X y = z ball D r z X z y | z X y = z ball D r
46 40 45 sylibr D Met X J Comp r + X y | z X y = z ball D r
47 29 46 eqsstrrd D Met X J Comp r + J y | z X y = z ball D r
48 26 unissd D Met X J Comp r + y | z X y = z ball D r J
49 47 48 eqssd D Met X J Comp r + J = y | z X y = z ball D r
50 eqid J = J
51 50 cmpcov J Comp y | z X y = z ball D r J J = y | z X y = z ball D r x 𝒫 y | z X y = z ball D r Fin J = x
52 14 26 49 51 syl3anc D Met X J Comp r + x 𝒫 y | z X y = z ball D r Fin J = x
53 elin x 𝒫 y | z X y = z ball D r Fin x 𝒫 y | z X y = z ball D r x Fin
54 ancom x 𝒫 y | z X y = z ball D r x Fin x Fin x 𝒫 y | z X y = z ball D r
55 53 54 bitri x 𝒫 y | z X y = z ball D r Fin x Fin x 𝒫 y | z X y = z ball D r
56 55 anbi1i x 𝒫 y | z X y = z ball D r Fin J = x x Fin x 𝒫 y | z X y = z ball D r J = x
57 anass x Fin x 𝒫 y | z X y = z ball D r J = x x Fin x 𝒫 y | z X y = z ball D r J = x
58 56 57 bitri x 𝒫 y | z X y = z ball D r Fin J = x x Fin x 𝒫 y | z X y = z ball D r J = x
59 58 rexbii2 x 𝒫 y | z X y = z ball D r Fin J = x x Fin x 𝒫 y | z X y = z ball D r J = x
60 52 59 sylib D Met X J Comp r + x Fin x 𝒫 y | z X y = z ball D r J = x
61 ancom x 𝒫 y | z X y = z ball D r J = x J = x x 𝒫 y | z X y = z ball D r
62 eqcom x = X X = x
63 29 eqeq1d D Met X J Comp r + X = x J = x
64 62 63 bitr2id D Met X J Comp r + J = x x = X
65 64 anbi1d D Met X J Comp r + J = x x 𝒫 y | z X y = z ball D r x = X x 𝒫 y | z X y = z ball D r
66 61 65 syl5bb D Met X J Comp r + x 𝒫 y | z X y = z ball D r J = x x = X x 𝒫 y | z X y = z ball D r
67 elpwi x 𝒫 y | z X y = z ball D r x y | z X y = z ball D r
68 ssabral x y | z X y = z ball D r y x z X y = z ball D r
69 67 68 sylib x 𝒫 y | z X y = z ball D r y x z X y = z ball D r
70 69 anim2i x = X x 𝒫 y | z X y = z ball D r x = X y x z X y = z ball D r
71 66 70 syl6bi D Met X J Comp r + x 𝒫 y | z X y = z ball D r J = x x = X y x z X y = z ball D r
72 71 reximdv D Met X J Comp r + x Fin x 𝒫 y | z X y = z ball D r J = x x Fin x = X y x z X y = z ball D r
73 60 72 mpd D Met X J Comp r + x Fin x = X y x z X y = z ball D r
74 73 ralrimiva D Met X J Comp r + x Fin x = X y x z X y = z ball D r
75 istotbnd D TotBnd X D Met X r + x Fin x = X y x z X y = z ball D r
76 11 74 75 sylanbrc D Met X J Comp D TotBnd X
77 13 76 jca D Met X J Comp D CMet X D TotBnd X