Metamath Proof Explorer

Theorem sstotbnd

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 
|- N = ( M |` ( Y X. Y ) )
Assertion sstotbnd 
|- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )

Proof

Step Hyp Ref Expression
1 sstotbnd.2 
 |-  N = ( M |` ( Y X. Y ) )
2 1 sstotbnd2 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) )
3 elfpw 
 |-  ( u e. ( ~P X i^i Fin ) <-> ( u C_ X /\ u e. Fin ) )
4 3 simprbi 
 |-  ( u e. ( ~P X i^i Fin ) -> u e. Fin )
5 mptfi 
 |-  ( u e. Fin -> ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin )
6 rnfi 
 |-  ( ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin )
7 4 5 6 3syl 
 |-  ( u e. ( ~P X i^i Fin ) -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin )
8 7 ad2antrl 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin )
9 simprr 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> Y C_ U_ x e. u ( x ( ball ` M ) d ) )
10 eqid 
 |-  ( x e. u |-> ( x ( ball ` M ) d ) ) = ( x e. u |-> ( x ( ball ` M ) d ) )
11 10 rnmpt 
 |-  ran ( x e. u |-> ( x ( ball ` M ) d ) ) = { b | E. x e. u b = ( x ( ball ` M ) d ) }
12 3 simplbi 
 |-  ( u e. ( ~P X i^i Fin ) -> u C_ X )
13 ssrexv 
 |-  ( u C_ X -> ( E. x e. u b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) )
14 12 13 syl 
 |-  ( u e. ( ~P X i^i Fin ) -> ( E. x e. u b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) )
15 14 ad2antrl 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> ( E. x e. u b = ( x ( ball ` M ) d ) -> E. x e. X b = ( x ( ball ` M ) d ) ) )
16 15 ss2abdv 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> { b | E. x e. u b = ( x ( ball ` M ) d ) } C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } )
17 11 16 eqsstrid 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } )
18 unieq 
 |-  ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> U. v = U. ran ( x e. u |-> ( x ( ball ` M ) d ) ) )
19 ovex 
 |-  ( x ( ball ` M ) d ) e. _V
20 19 dfiun3 
 |-  U_ x e. u ( x ( ball ` M ) d ) = U. ran ( x e. u |-> ( x ( ball ` M ) d ) )
21 18 20 eqtr4di 
 |-  ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> U. v = U_ x e. u ( x ( ball ` M ) d ) )
22 21 sseq2d 
 |-  ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( Y C_ U. v <-> Y C_ U_ x e. u ( x ( ball ` M ) d ) ) )
23 ssabral 
 |-  ( v C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } <-> A. b e. v E. x e. X b = ( x ( ball ` M ) d ) )
24 sseq1 
 |-  ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( v C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } <-> ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) )
25 23 24 bitr3id 
 |-  ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( A. b e. v E. x e. X b = ( x ( ball ` M ) d ) <-> ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) )
26 22 25 anbi12d 
 |-  ( v = ran ( x e. u |-> ( x ( ball ` M ) d ) ) -> ( ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) <-> ( Y C_ U_ x e. u ( x ( ball ` M ) d ) /\ ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) )
27 26 rspcev 
 |-  ( ( ran ( x e. u |-> ( x ( ball ` M ) d ) ) e. Fin /\ ( Y C_ U_ x e. u ( x ( ball ` M ) d ) /\ ran ( x e. u |-> ( x ( ball ` M ) d ) ) C_ { b | E. x e. X b = ( x ( ball ` M ) d ) } ) ) -> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) )
28 8 9 17 27 syl12anc 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( u e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. u ( x ( ball ` M ) d ) ) ) -> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) )
29 28 rexlimdvaa 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) -> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
30 oveq1 
 |-  ( x = ( f ` b ) -> ( x ( ball ` M ) d ) = ( ( f ` b ) ( ball ` M ) d ) )
31 30 eqeq2d 
 |-  ( x = ( f ` b ) -> ( b = ( x ( ball ` M ) d ) <-> b = ( ( f ` b ) ( ball ` M ) d ) ) )
32 31 ac6sfi 
 |-  ( ( v e. Fin /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> E. f ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) )
33 32 adantrl 
 |-  ( ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) -> E. f ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) )
34 33 adantl 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) -> E. f ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) )
35 frn 
 |-  ( f : v --> X -> ran f C_ X )
36 35 ad2antrl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> ran f C_ X )
37 simplrl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> v e. Fin )
38 ffn 
 |-  ( f : v --> X -> f Fn v )
39 38 ad2antrl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> f Fn v )
40 dffn4 
 |-  ( f Fn v <-> f : v -onto-> ran f )
41 39 40 sylib 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> f : v -onto-> ran f )
42 fofi 
 |-  ( ( v e. Fin /\ f : v -onto-> ran f ) -> ran f e. Fin )
43 37 41 42 syl2anc 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> ran f e. Fin )
44 elfpw 
 |-  ( ran f e. ( ~P X i^i Fin ) <-> ( ran f C_ X /\ ran f e. Fin ) )
45 36 43 44 sylanbrc 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> ran f e. ( ~P X i^i Fin ) )
46 simprrl 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) -> Y C_ U. v )
47 46 adantr 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> Y C_ U. v )
48 uniiun 
 |-  U. v = U_ b e. v b
49 iuneq2 
 |-  ( A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) -> U_ b e. v b = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) )
50 48 49 syl5eq 
 |-  ( A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) -> U. v = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) )
51 50 ad2antll 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> U. v = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) )
52 47 51 sseqtrd 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> Y C_ U_ b e. v ( ( f ` b ) ( ball ` M ) d ) )
53 30 eleq2d 
 |-  ( x = ( f ` b ) -> ( y e. ( x ( ball ` M ) d ) <-> y e. ( ( f ` b ) ( ball ` M ) d ) ) )
54 53 rexrn 
 |-  ( f Fn v -> ( E. x e. ran f y e. ( x ( ball ` M ) d ) <-> E. b e. v y e. ( ( f ` b ) ( ball ` M ) d ) ) )
55 eliun 
 |-  ( y e. U_ x e. ran f ( x ( ball ` M ) d ) <-> E. x e. ran f y e. ( x ( ball ` M ) d ) )
56 eliun 
 |-  ( y e. U_ b e. v ( ( f ` b ) ( ball ` M ) d ) <-> E. b e. v y e. ( ( f ` b ) ( ball ` M ) d ) )
57 54 55 56 3bitr4g 
 |-  ( f Fn v -> ( y e. U_ x e. ran f ( x ( ball ` M ) d ) <-> y e. U_ b e. v ( ( f ` b ) ( ball ` M ) d ) ) )
58 57 eqrdv 
 |-  ( f Fn v -> U_ x e. ran f ( x ( ball ` M ) d ) = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) )
59 39 58 syl 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> U_ x e. ran f ( x ( ball ` M ) d ) = U_ b e. v ( ( f ` b ) ( ball ` M ) d ) )
60 52 59 sseqtrrd 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> Y C_ U_ x e. ran f ( x ( ball ` M ) d ) )
61 iuneq1 
 |-  ( u = ran f -> U_ x e. u ( x ( ball ` M ) d ) = U_ x e. ran f ( x ( ball ` M ) d ) )
62 61 sseq2d 
 |-  ( u = ran f -> ( Y C_ U_ x e. u ( x ( ball ` M ) d ) <-> Y C_ U_ x e. ran f ( x ( ball ` M ) d ) ) )
63 62 rspcev 
 |-  ( ( ran f e. ( ~P X i^i Fin ) /\ Y C_ U_ x e. ran f ( x ( ball ` M ) d ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) )
64 45 60 63 syl2anc 
 |-  ( ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) /\ ( f : v --> X /\ A. b e. v b = ( ( f ` b ) ( ball ` M ) d ) ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) )
65 34 64 exlimddv 
 |-  ( ( ( M e. ( Met ` X ) /\ Y C_ X ) /\ ( v e. Fin /\ ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) )
66 65 rexlimdvaa 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) ) )
67 29 66 impbid 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) <-> E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
68 67 ralbidv 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( A. d e. RR+ E. u e. ( ~P X i^i Fin ) Y C_ U_ x e. u ( x ( ball ` M ) d ) <-> A. d e. RR+ E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
69 2 68 bitrd 
 |-  ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )