MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovresd Unicode version

Theorem ovresd 6443
Description: Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
ovresd.1
ovresd.2
Assertion
Ref Expression
ovresd

Proof of Theorem ovresd
StepHypRef Expression
1 ovresd.1 . 2
2 ovresd.2 . 2
3 ovres 6442 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  X.cxp 5002  |`cres 5006  (class class class)co 6296
This theorem is referenced by:  sscres  15192  fullsubc  15219  fullresc  15220  funcres2c  15270  psmetres2  20818  xmetres2  20864  prdsdsf  20870  xpsdsval  20884  xmssym  20968  xmstri2  20969  mstri2  20970  xmstri  20971  mstri  20972  xmstri3  20973  mstri3  20974  msrtri  20975  tmsxpsval  21041  ngptgp  21150  nlmvscn  21196  nrginvrcn  21200  nghmcn  21252  cnmpt1ds  21347  cnmpt2ds  21348  ipcn  21686  caussi  21736  causs  21737  minveclem2  21841  minveclem3b  21843  minveclem3  21844  minveclem4  21847  minveclem6  21849  ftc1lem6  22442  ulmdvlem1  22795  abelth  22836  cxpcn3  23122  rlimcnp  23295  hhssnv  26180  qqhcn  27972  qqhucn  27973  ftc1cnnc  30089  ismtyres  30304  isdrngo2  30361  rngchom  32775  ringchom  32821  irinitoringc  32877  rhmsubclem4  32897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-res 5016  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator