Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  totbndmet Structured version   Unicode version

Theorem totbndmet 29860
 Description: The predicate "totally bounded" implies is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
totbndmet

Proof of Theorem totbndmet
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istotbnd 29857 . 2
21simplbi 460 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1374   wcel 1762  wral 2809  wrex 2810  cuni 4240  cfv 5581  (class class class)co 6277  cfn 7508  crp 11211  cme 18170  cbl 18171  ctotbnd 29854 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-mpt 4502  df-id 4790  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-iota 5544  df-fun 5583  df-fv 5589  df-ov 6280  df-totbnd 29856 This theorem is referenced by:  totbndss  29865  totbndbnd  29877  prdstotbnd  29882
 Copyright terms: Public domain W3C validator