This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( Met ` X ) /\ J e. Comp ) <-> ( D e. ( CMet ` X ) /\ D e. ( TotBnd ` X ) ) )

Proof

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