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 ) ) ) )