Metamath Proof Explorer


Theorem heibor

Description: Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 and heiborlem1 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jan-2014)

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

Proof

Step Hyp Ref Expression
1 heibor.1 J = MetOpen D
2 1 heibor1 D Met X J Comp D CMet X D TotBnd X
3 cmetmet D CMet X D Met X
4 3 adantr D CMet X D TotBnd X D Met X
5 metxmet D Met X D ∞Met X
6 1 mopntop D ∞Met X J Top
7 3 5 6 3syl D CMet X J Top
8 7 adantr D CMet X D TotBnd X J Top
9 istotbnd D TotBnd X D Met X r + u Fin u = X v u y X v = y ball D r
10 9 simprbi D TotBnd X r + u Fin u = X v u y X v = y ball D r
11 2nn 2
12 nnexpcl 2 n 0 2 n
13 11 12 mpan n 0 2 n
14 13 nnrpd n 0 2 n +
15 14 rpreccld n 0 1 2 n +
16 oveq2 r = 1 2 n y ball D r = y ball D 1 2 n
17 16 eqeq2d r = 1 2 n v = y ball D r v = y ball D 1 2 n
18 17 rexbidv r = 1 2 n y X v = y ball D r y X v = y ball D 1 2 n
19 18 ralbidv r = 1 2 n v u y X v = y ball D r v u y X v = y ball D 1 2 n
20 19 anbi2d r = 1 2 n u = X v u y X v = y ball D r u = X v u y X v = y ball D 1 2 n
21 20 rexbidv r = 1 2 n u Fin u = X v u y X v = y ball D r u Fin u = X v u y X v = y ball D 1 2 n
22 21 rspccva r + u Fin u = X v u y X v = y ball D r 1 2 n + u Fin u = X v u y X v = y ball D 1 2 n
23 10 15 22 syl2an D TotBnd X n 0 u Fin u = X v u y X v = y ball D 1 2 n
24 23 expcom n 0 D TotBnd X u Fin u = X v u y X v = y ball D 1 2 n
25 24 adantl D CMet X n 0 D TotBnd X u Fin u = X v u y X v = y ball D 1 2 n
26 oveq1 y = m v y ball D 1 2 n = m v ball D 1 2 n
27 26 eqeq2d y = m v v = y ball D 1 2 n v = m v ball D 1 2 n
28 27 ac6sfi u Fin v u y X v = y ball D 1 2 n m m : u X v u v = m v ball D 1 2 n
29 28 adantrl u Fin u = X v u y X v = y ball D 1 2 n m m : u X v u v = m v ball D 1 2 n
30 29 adantl D CMet X n 0 u Fin u = X v u y X v = y ball D 1 2 n m m : u X v u v = m v ball D 1 2 n
31 simp3l D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n m : u X
32 31 frnd D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n ran m X
33 1 mopnuni D ∞Met X X = J
34 3 5 33 3syl D CMet X X = J
35 34 adantr D CMet X n 0 X = J
36 35 3ad2ant1 D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n X = J
37 32 36 sseqtrd D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n ran m J
38 1 fvexi J V
39 38 uniex J V
40 39 elpw2 ran m 𝒫 J ran m J
41 37 40 sylibr D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n ran m 𝒫 J
42 simp2l D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n u Fin
43 ffn m : u X m Fn u
44 dffn4 m Fn u m : u onto ran m
45 43 44 sylib m : u X m : u onto ran m
46 fofi u Fin m : u onto ran m ran m Fin
47 45 46 sylan2 u Fin m : u X ran m Fin
48 42 31 47 syl2anc D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n ran m Fin
49 41 48 elind D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n ran m 𝒫 J Fin
50 26 eleq2d y = m v r y ball D 1 2 n r m v ball D 1 2 n
51 50 rexrn m Fn u y ran m r y ball D 1 2 n v u r m v ball D 1 2 n
52 eliun r y ran m y ball D 1 2 n y ran m r y ball D 1 2 n
53 eliun r v u m v ball D 1 2 n v u r m v ball D 1 2 n
54 51 52 53 3bitr4g m Fn u r y ran m y ball D 1 2 n r v u m v ball D 1 2 n
55 54 eqrdv m Fn u y ran m y ball D 1 2 n = v u m v ball D 1 2 n
56 31 43 55 3syl D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n y ran m y ball D 1 2 n = v u m v ball D 1 2 n
57 simp3r D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n v u v = m v ball D 1 2 n
58 uniiun u = v u v
59 iuneq2 v u v = m v ball D 1 2 n v u v = v u m v ball D 1 2 n
60 58 59 syl5eq v u v = m v ball D 1 2 n u = v u m v ball D 1 2 n
61 57 60 syl D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n u = v u m v ball D 1 2 n
62 simp2r D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n u = X
63 56 61 62 3eqtr2rd D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n X = y ran m y ball D 1 2 n
64 iuneq1 t = ran m y t y ball D 1 2 n = y ran m y ball D 1 2 n
65 64 rspceeqv ran m 𝒫 J Fin X = y ran m y ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
66 49 63 65 syl2anc D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
67 66 3expia D CMet X n 0 u Fin u = X m : u X v u v = m v ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
68 67 adantrrr D CMet X n 0 u Fin u = X v u y X v = y ball D 1 2 n m : u X v u v = m v ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
69 68 exlimdv D CMet X n 0 u Fin u = X v u y X v = y ball D 1 2 n m m : u X v u v = m v ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
70 30 69 mpd D CMet X n 0 u Fin u = X v u y X v = y ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
71 70 rexlimdvaa D CMet X n 0 u Fin u = X v u y X v = y ball D 1 2 n t 𝒫 J Fin X = y t y ball D 1 2 n
72 25 71 syld D CMet X n 0 D TotBnd X t 𝒫 J Fin X = y t y ball D 1 2 n
73 72 ralrimdva D CMet X D TotBnd X n 0 t 𝒫 J Fin X = y t y ball D 1 2 n
74 39 pwex 𝒫 J V
75 74 inex1 𝒫 J Fin V
76 nn0ennn 0
77 nnenom ω
78 76 77 entri 0 ω
79 iuneq1 t = m n y t y ball D 1 2 n = y m n y ball D 1 2 n
80 79 eqeq2d t = m n X = y t y ball D 1 2 n X = y m n y ball D 1 2 n
81 75 78 80 axcc4 n 0 t 𝒫 J Fin X = y t y ball D 1 2 n m m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n
82 73 81 syl6 D CMet X D TotBnd X m m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n
83 elpwi r 𝒫 J r J
84 eqid u | ¬ v 𝒫 r Fin u v = u | ¬ v 𝒫 r Fin u v
85 eqid t k | k 0 t m k t z X , m 0 z ball D 1 2 m k u | ¬ v 𝒫 r Fin u v = t k | k 0 t m k t z X , m 0 z ball D 1 2 m k u | ¬ v 𝒫 r Fin u v
86 eqid z X , m 0 z ball D 1 2 m = z X , m 0 z ball D 1 2 m
87 simpl D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n D CMet X
88 34 pweqd D CMet X 𝒫 X = 𝒫 J
89 88 ineq1d D CMet X 𝒫 X Fin = 𝒫 J Fin
90 89 feq3d D CMet X m : 0 𝒫 X Fin m : 0 𝒫 J Fin
91 90 biimpar D CMet X m : 0 𝒫 J Fin m : 0 𝒫 X Fin
92 91 adantrr D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n m : 0 𝒫 X Fin
93 oveq1 t = y t z X , m 0 z ball D 1 2 m n = y z X , m 0 z ball D 1 2 m n
94 93 cbviunv t m n t z X , m 0 z ball D 1 2 m n = y m n y z X , m 0 z ball D 1 2 m n
95 id m : 0 𝒫 J Fin m : 0 𝒫 J Fin
96 inss1 𝒫 J Fin 𝒫 J
97 96 88 sseqtrrid D CMet X 𝒫 J Fin 𝒫 X
98 fss m : 0 𝒫 J Fin 𝒫 J Fin 𝒫 X m : 0 𝒫 X
99 95 97 98 syl2anr D CMet X m : 0 𝒫 J Fin m : 0 𝒫 X
100 99 ffvelrnda D CMet X m : 0 𝒫 J Fin n 0 m n 𝒫 X
101 100 elpwid D CMet X m : 0 𝒫 J Fin n 0 m n X
102 101 sselda D CMet X m : 0 𝒫 J Fin n 0 y m n y X
103 simplr D CMet X m : 0 𝒫 J Fin n 0 y m n n 0
104 oveq1 z = y z ball D 1 2 m = y ball D 1 2 m
105 oveq2 m = n 2 m = 2 n
106 105 oveq2d m = n 1 2 m = 1 2 n
107 106 oveq2d m = n y ball D 1 2 m = y ball D 1 2 n
108 ovex y ball D 1 2 n V
109 104 107 86 108 ovmpo y X n 0 y z X , m 0 z ball D 1 2 m n = y ball D 1 2 n
110 102 103 109 syl2anc D CMet X m : 0 𝒫 J Fin n 0 y m n y z X , m 0 z ball D 1 2 m n = y ball D 1 2 n
111 110 iuneq2dv D CMet X m : 0 𝒫 J Fin n 0 y m n y z X , m 0 z ball D 1 2 m n = y m n y ball D 1 2 n
112 94 111 syl5eq D CMet X m : 0 𝒫 J Fin n 0 t m n t z X , m 0 z ball D 1 2 m n = y m n y ball D 1 2 n
113 112 eqeq2d D CMet X m : 0 𝒫 J Fin n 0 X = t m n t z X , m 0 z ball D 1 2 m n X = y m n y ball D 1 2 n
114 113 biimprd D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n X = t m n t z X , m 0 z ball D 1 2 m n
115 114 ralimdva D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n n 0 X = t m n t z X , m 0 z ball D 1 2 m n
116 115 impr D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n n 0 X = t m n t z X , m 0 z ball D 1 2 m n
117 fveq2 n = k m n = m k
118 117 iuneq1d n = k t m n t z X , m 0 z ball D 1 2 m n = t m k t z X , m 0 z ball D 1 2 m n
119 simpl n = k t m k n = k
120 119 oveq2d n = k t m k t z X , m 0 z ball D 1 2 m n = t z X , m 0 z ball D 1 2 m k
121 120 iuneq2dv n = k t m k t z X , m 0 z ball D 1 2 m n = t m k t z X , m 0 z ball D 1 2 m k
122 118 121 eqtrd n = k t m n t z X , m 0 z ball D 1 2 m n = t m k t z X , m 0 z ball D 1 2 m k
123 122 eqeq2d n = k X = t m n t z X , m 0 z ball D 1 2 m n X = t m k t z X , m 0 z ball D 1 2 m k
124 123 cbvralvw n 0 X = t m n t z X , m 0 z ball D 1 2 m n k 0 X = t m k t z X , m 0 z ball D 1 2 m k
125 116 124 sylib D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n k 0 X = t m k t z X , m 0 z ball D 1 2 m k
126 1 84 85 86 87 92 125 heiborlem10 D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n r J J = r v 𝒫 r Fin J = v
127 126 exp32 D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n r J J = r v 𝒫 r Fin J = v
128 83 127 syl5 D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n r 𝒫 J J = r v 𝒫 r Fin J = v
129 128 ralrimiv D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n r 𝒫 J J = r v 𝒫 r Fin J = v
130 129 ex D CMet X m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n r 𝒫 J J = r v 𝒫 r Fin J = v
131 130 exlimdv D CMet X m m : 0 𝒫 J Fin n 0 X = y m n y ball D 1 2 n r 𝒫 J J = r v 𝒫 r Fin J = v
132 82 131 syld D CMet X D TotBnd X r 𝒫 J J = r v 𝒫 r Fin J = v
133 132 imp D CMet X D TotBnd X r 𝒫 J J = r v 𝒫 r Fin J = v
134 eqid J = J
135 134 iscmp J Comp J Top r 𝒫 J J = r v 𝒫 r Fin J = v
136 8 133 135 sylanbrc D CMet X D TotBnd X J Comp
137 4 136 jca D CMet X D TotBnd X D Met X J Comp
138 2 137 impbii D Met X J Comp D CMet X D TotBnd X