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