Metamath Proof Explorer

Theorem istotbnd3

Description: A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion istotbnd3 
|- ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )

Proof

Step Hyp Ref Expression
1 istotbnd 
 |-  ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) ) )
2 oveq1 
 |-  ( x = ( f ` b ) -> ( x ( ball ` M ) d ) = ( ( f ` b ) ( ball ` M ) d ) )
3 2 eqeq2d 
 |-  ( x = ( f ` b ) -> ( b = ( x ( ball ` M ) d ) <-> b = ( ( f ` b ) ( ball ` M ) d ) ) )
4 3 ac6sfi 
 |-  ( ( w e. Fin /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) -> E. f ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) )
5 4 ex 
 |-  ( w e. Fin -> ( A. b e. w E. x e. X b = ( x ( ball ` M ) d ) -> E. f ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) )
6 5 ad2antlr 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ U. w = X ) -> ( A. b e. w E. x e. X b = ( x ( ball ` M ) d ) -> E. f ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) )
7 simprrl 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> f : w --> X )
8 7 frnd 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> ran f C_ X )
9 simplr 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> w e. Fin )
10 7 ffnd 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> f Fn w )
11 dffn4 
 |-  ( f Fn w <-> f : w -onto-> ran f )
12 10 11 sylib 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> f : w -onto-> ran f )
13 fofi 
 |-  ( ( w e. Fin /\ f : w -onto-> ran f ) -> ran f e. Fin )
14 9 12 13 syl2anc 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> ran f e. Fin )
15 elfpw 
 |-  ( ran f e. ( ~P X i^i Fin ) <-> ( ran f C_ X /\ ran f e. Fin ) )
16 8 14 15 sylanbrc 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> ran f e. ( ~P X i^i Fin ) )
17 2 eleq2d 
 |-  ( x = ( f ` b ) -> ( v e. ( x ( ball ` M ) d ) <-> v e. ( ( f ` b ) ( ball ` M ) d ) ) )
18 17 rexrn 
 |-  ( f Fn w -> ( E. x e. ran f v e. ( x ( ball ` M ) d ) <-> E. b e. w v e. ( ( f ` b ) ( ball ` M ) d ) ) )
19 10 18 syl 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> ( E. x e. ran f v e. ( x ( ball ` M ) d ) <-> E. b e. w v e. ( ( f ` b ) ( ball ` M ) d ) ) )
20 eliun 
 |-  ( v e. U_ x e. ran f ( x ( ball ` M ) d ) <-> E. x e. ran f v e. ( x ( ball ` M ) d ) )
21 eliun 
 |-  ( v e. U_ b e. w ( ( f ` b ) ( ball ` M ) d ) <-> E. b e. w v e. ( ( f ` b ) ( ball ` M ) d ) )
22 19 20 21 3bitr4g 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> ( v e. U_ x e. ran f ( x ( ball ` M ) d ) <-> v e. U_ b e. w ( ( f ` b ) ( ball ` M ) d ) ) )
23 22 eqrdv 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> U_ x e. ran f ( x ( ball ` M ) d ) = U_ b e. w ( ( f ` b ) ( ball ` M ) d ) )
24 simprrr 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) )
25 iuneq2 
 |-  ( A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) -> U_ b e. w b = U_ b e. w ( ( f ` b ) ( ball ` M ) d ) )
26 24 25 syl 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> U_ b e. w b = U_ b e. w ( ( f ` b ) ( ball ` M ) d ) )
27 uniiun 
 |-  U. w = U_ b e. w b
28 simprl 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> U. w = X )
29 27 28 eqtr3id 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> U_ b e. w b = X )
30 23 26 29 3eqtr2d 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> U_ x e. ran f ( x ( ball ` M ) d ) = X )
31 iuneq1 
 |-  ( v = ran f -> U_ x e. v ( x ( ball ` M ) d ) = U_ x e. ran f ( x ( ball ` M ) d ) )
32 31 eqeq1d 
 |-  ( v = ran f -> ( U_ x e. v ( x ( ball ` M ) d ) = X <-> U_ x e. ran f ( x ( ball ` M ) d ) = X ) )
33 32 rspcev 
 |-  ( ( ran f e. ( ~P X i^i Fin ) /\ U_ x e. ran f ( x ( ball ` M ) d ) = X ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X )
34 16 30 33 syl2anc 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ ( U. w = X /\ ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) ) ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X )
35 34 expr 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ U. w = X ) -> ( ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
36 35 exlimdv 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ U. w = X ) -> ( E. f ( f : w --> X /\ A. b e. w b = ( ( f ` b ) ( ball ` M ) d ) ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
37 6 36 syld 
 |-  ( ( ( M e. ( Met ` X ) /\ w e. Fin ) /\ U. w = X ) -> ( A. b e. w E. x e. X b = ( x ( ball ` M ) d ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
38 37 expimpd 
 |-  ( ( M e. ( Met ` X ) /\ w e. Fin ) -> ( ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
39 38 rexlimdva 
 |-  ( M e. ( Met ` X ) -> ( E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
40 elfpw 
 |-  ( v e. ( ~P X i^i Fin ) <-> ( v C_ X /\ v e. Fin ) )
41 40 simprbi 
 |-  ( v e. ( ~P X i^i Fin ) -> v e. Fin )
42 41 ad2antrl 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> v e. Fin )
43 mptfi 
 |-  ( v e. Fin -> ( x e. v |-> ( x ( ball ` M ) d ) ) e. Fin )
44 rnfi 
 |-  ( ( x e. v |-> ( x ( ball ` M ) d ) ) e. Fin -> ran ( x e. v |-> ( x ( ball ` M ) d ) ) e. Fin )
45 42 43 44 3syl 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> ran ( x e. v |-> ( x ( ball ` M ) d ) ) e. Fin )
46 ovex 
 |-  ( x ( ball ` M ) d ) e. _V
47 46 dfiun3 
 |-  U_ x e. v ( x ( ball ` M ) d ) = U. ran ( x e. v |-> ( x ( ball ` M ) d ) )
48 simprr 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> U_ x e. v ( x ( ball ` M ) d ) = X )
49 47 48 eqtr3id 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> U. ran ( x e. v |-> ( x ( ball ` M ) d ) ) = X )
50 eqid 
 |-  ( x e. v |-> ( x ( ball ` M ) d ) ) = ( x e. v |-> ( x ( ball ` M ) d ) )
51 50 rnmpt 
 |-  ran ( x e. v |-> ( x ( ball ` M ) d ) ) = { b | E. x e. v b = ( x ( ball ` M ) d ) }
52 40 simplbi 
 |-  ( v e. ( ~P X i^i Fin ) -> v C_ X )
53 52 ad2antrl 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> v C_ X )
54 ssrexv 
 |-  ( v C_ X -> ( E. x e. v b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) )
55 53 54 syl 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> ( E. x e. v b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) )
56 55 ss2abdv 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> { b | E. x e. v b = ( x ( ball ` M ) d ) } C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } )
57 51 56 eqsstrid 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> ran ( x e. v |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } )
58 unieq 
 |-  ( w = ran ( x e. v |-> ( x ( ball ` M ) d ) ) -> U. w = U. ran ( x e. v |-> ( x ( ball ` M ) d ) ) )
59 58 eqeq1d 
 |-  ( w = ran ( x e. v |-> ( x ( ball ` M ) d ) ) -> ( U. w = X <-> U. ran ( x e. v |-> ( x ( ball ` M ) d ) ) = X ) )
60 ssabral 
 |-  ( w C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } <-> A. b e. w E. x e. X b = ( x ( ball ` M ) d ) )
61 sseq1 
 |-  ( w = ran ( x e. v |-> ( x ( ball ` M ) d ) ) -> ( w C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } <-> ran ( x e. v |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) )
62 60 61 bitr3id 
 |-  ( w = ran ( x e. v |-> ( x ( ball ` M ) d ) ) -> ( A. b e. w E. x e. X b = ( x ( ball ` M ) d ) <-> ran ( x e. v |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) )
63 59 62 anbi12d 
 |-  ( w = ran ( x e. v |-> ( x ( ball ` M ) d ) ) -> ( ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) <-> ( U. ran ( x e. v |-> ( x ( ball ` M ) d ) ) = X /\ ran ( x e. v |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) )
64 63 rspcev 
 |-  ( ( ran ( x e. v |-> ( x ( ball ` M ) d ) ) e. Fin /\ ( U. ran ( x e. v |-> ( x ( ball ` M ) d ) ) = X /\ ran ( x e. v |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) -> E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) )
65 45 49 57 64 syl12anc 
 |-  ( ( M e. ( Met ` X ) /\ ( v e. ( ~P X i^i Fin ) /\ U_ x e. v ( x ( ball ` M ) d ) = X ) ) -> E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) )
66 65 expr 
 |-  ( ( M e. ( Met ` X ) /\ v e. ( ~P X i^i Fin ) ) -> ( U_ x e. v ( x ( ball ` M ) d ) = X -> E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) ) )
67 66 rexlimdva 
 |-  ( M e. ( Met ` X ) -> ( E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X -> E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) ) )
68 39 67 impbid 
 |-  ( M e. ( Met ` X ) -> ( E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) <-> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
69 68 ralbidv 
 |-  ( M e. ( Met ` X ) -> ( A. d e. RR+ E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) <-> A. d e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
70 69 pm5.32i 
 |-  ( ( M e. ( Met ` X ) /\ A. d e. RR+ E. w e. Fin ( U. w = X /\ A. b e. w E. x e. X b = ( x ( ball ` M ) d ) ) ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
71 1 70 bitri 
 |-  ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )