Metamath Proof Explorer

Theorem equivtotbnd

Description: If the metric M is "strongly finer" than N (meaning that there is a positive real constant R such that N ( x , y ) <_ R x. M ( x , y ) ), then total boundedness of M implies total boundedness of N . (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses equivtotbnd.1 
|- ( ph -> M e. ( TotBnd ` X ) )
equivtotbnd.2 
|- ( ph -> N e. ( Met ` X ) )
equivtotbnd.3 
|- ( ph -> R e. RR+ )
equivtotbnd.4 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
Assertion equivtotbnd 
|- ( ph -> N e. ( TotBnd ` X ) )

Proof

Step Hyp Ref Expression
1 equivtotbnd.1 
 |-  ( ph -> M e. ( TotBnd ` X ) )
2 equivtotbnd.2 
 |-  ( ph -> N e. ( Met ` X ) )
3 equivtotbnd.3 
 |-  ( ph -> R e. RR+ )
4 equivtotbnd.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )
5 simpr 
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR+ )
6 3 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> R e. RR+ )
7 5 6 rpdivcld 
 |-  ( ( ph /\ r e. RR+ ) -> ( r / R ) e. RR+ )
8 1 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> M e. ( TotBnd ` X ) )
9 istotbnd3 
 |-  ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. s e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) s ) = X ) )
10 9 simprbi 
 |-  ( M e. ( TotBnd ` X ) -> A. s e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) s ) = X )
11 8 10 syl 
 |-  ( ( ph /\ r e. RR+ ) -> A. s e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) s ) = X )
12 oveq2 
 |-  ( s = ( r / R ) -> ( x ( ball ` M ) s ) = ( x ( ball ` M ) ( r / R ) ) )
13 12 iuneq2d 
 |-  ( s = ( r / R ) -> U_ x e. v ( x ( ball ` M ) s ) = U_ x e. v ( x ( ball ` M ) ( r / R ) ) )
14 13 eqeq1d 
 |-  ( s = ( r / R ) -> ( U_ x e. v ( x ( ball ` M ) s ) = X <-> U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X ) )
15 14 rexbidv 
 |-  ( s = ( r / R ) -> ( E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) s ) = X <-> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X ) )
16 15 rspcv 
 |-  ( ( r / R ) e. RR+ -> ( A. s e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) s ) = X -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X ) )
17 7 11 16 sylc 
 |-  ( ( ph /\ r e. RR+ ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X )
18 elfpw 
 |-  ( v e. ( ~P X i^i Fin ) <-> ( v C_ X /\ v e. Fin ) )
19 18 simplbi 
 |-  ( v e. ( ~P X i^i Fin ) -> v C_ X )
20 19 adantl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> v C_ X )
21 20 sselda 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> x e. X )
22 eqid 
 |-  ( MetOpen ` N ) = ( MetOpen ` N )
23 eqid 
 |-  ( MetOpen ` M ) = ( MetOpen ` M )
24 9 simplbi 
 |-  ( M e. ( TotBnd ` X ) -> M e. ( Met ` X ) )
25 1 24 syl 
 |-  ( ph -> M e. ( Met ` X ) )
26 22 23 2 25 3 4 metss2lem 
 |-  ( ( ph /\ ( x e. X /\ r e. RR+ ) ) -> ( x ( ball ` M ) ( r / R ) ) C_ ( x ( ball ` N ) r ) )
27 26 anass1rs 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` M ) ( r / R ) ) C_ ( x ( ball ` N ) r ) )
28 27 adantlr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. X ) -> ( x ( ball ` M ) ( r / R ) ) C_ ( x ( ball ` N ) r ) )
29 21 28 syldan 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> ( x ( ball ` M ) ( r / R ) ) C_ ( x ( ball ` N ) r ) )
30 29 ralrimiva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> A. x e. v ( x ( ball ` M ) ( r / R ) ) C_ ( x ( ball ` N ) r ) )
31 ss2iun 
 |-  ( A. x e. v ( x ( ball ` M ) ( r / R ) ) C_ ( x ( ball ` N ) r ) -> U_ x e. v ( x ( ball ` M ) ( r / R ) ) C_ U_ x e. v ( x ( ball ` N ) r ) )
32 30 31 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> U_ x e. v ( x ( ball ` M ) ( r / R ) ) C_ U_ x e. v ( x ( ball ` N ) r ) )
33 sseq1 
 |-  ( U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X -> ( U_ x e. v ( x ( ball ` M ) ( r / R ) ) C_ U_ x e. v ( x ( ball ` N ) r ) <-> X C_ U_ x e. v ( x ( ball ` N ) r ) ) )
34 32 33 syl5ibcom 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> ( U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X -> X C_ U_ x e. v ( x ( ball ` N ) r ) ) )
35 2 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> N e. ( Met ` X ) )
36 metxmet 
 |-  ( N e. ( Met ` X ) -> N e. ( *Met ` X ) )
37 35 36 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> N e. ( *Met ` X ) )
38 simpllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> r e. RR+ )
39 38 rpxrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> r e. RR* )
40 blssm 
 |-  ( ( N e. ( *Met ` X ) /\ x e. X /\ r e. RR* ) -> ( x ( ball ` N ) r ) C_ X )
41 37 21 39 40 syl3anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) /\ x e. v ) -> ( x ( ball ` N ) r ) C_ X )
42 41 ralrimiva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> A. x e. v ( x ( ball ` N ) r ) C_ X )
43 iunss 
 |-  ( U_ x e. v ( x ( ball ` N ) r ) C_ X <-> A. x e. v ( x ( ball ` N ) r ) C_ X )
44 42 43 sylibr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> U_ x e. v ( x ( ball ` N ) r ) C_ X )
45 34 44 jctild 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> ( U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X -> ( U_ x e. v ( x ( ball ` N ) r ) C_ X /\ X C_ U_ x e. v ( x ( ball ` N ) r ) ) ) )
46 eqss 
 |-  ( U_ x e. v ( x ( ball ` N ) r ) = X <-> ( U_ x e. v ( x ( ball ` N ) r ) C_ X /\ X C_ U_ x e. v ( x ( ball ` N ) r ) ) )
47 45 46 syl6ibr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ v e. ( ~P X i^i Fin ) ) -> ( U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X -> U_ x e. v ( x ( ball ` N ) r ) = X ) )
48 47 reximdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) ( r / R ) ) = X -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` N ) r ) = X ) )
49 17 48 mpd 
 |-  ( ( ph /\ r e. RR+ ) -> E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` N ) r ) = X )
50 49 ralrimiva 
 |-  ( ph -> A. r e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` N ) r ) = X )
51 istotbnd3 
 |-  ( N e. ( TotBnd ` X ) <-> ( N e. ( Met ` X ) /\ A. r e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` N ) r ) = X ) )
52 2 50 51 sylanbrc 
 |-  ( ph -> N e. ( TotBnd ` X ) )