![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > metxmet | Structured version Visualization version GIF version |
Description: A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Ref | Expression |
---|---|
metxmet | ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismet2 22466 | . 2 ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ)) | |
2 | 1 | simplbi 492 | 1 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 × cxp 5310 ⟶wf 6097 ‘cfv 6101 ℝcr 10223 ∞Metcxmet 20053 Metcmet 20054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-mulcl 10286 ax-i2m1 10292 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-er 7982 df-map 8097 df-en 8196 df-dom 8197 df-sdom 8198 df-pnf 10365 df-mnf 10366 df-xr 10367 df-xadd 12194 df-xmet 20061 df-met 20062 |
This theorem is referenced by: metdmdm 22469 meteq0 22472 mettri2 22474 met0 22476 metge0 22478 metsym 22483 metrtri 22490 metgt0 22492 metres2 22496 prdsmet 22503 imasf1omet 22509 blpnf 22530 bl2in 22533 isms2 22583 setsms 22613 tmsms 22620 metss2lem 22644 metss2 22645 methaus 22653 dscopn 22706 ngpocelbl 22836 cnxmet 22904 rexmet 22922 metdcn2 22970 metdsre 22984 metdscn2 22988 lebnumlem1 23088 lebnumlem2 23089 lebnumlem3 23090 lebnum 23091 xlebnum 23092 cmetcaulem 23414 cmetcau 23415 iscmet3lem1 23417 iscmet3lem2 23418 iscmet3 23419 equivcfil 23425 equivcau 23426 metsscmetcld 23441 cmetss 23442 relcmpcmet 23444 cmpcmet 23445 cncmet 23448 bcthlem2 23451 bcthlem3 23452 bcthlem4 23453 bcthlem5 23454 bcth2 23456 bcth3 23457 cmetcusp1 23479 cmetcusp 23480 minveclem3 23539 imsxmet 28072 blocni 28185 ubthlem1 28251 ubthlem2 28252 minvecolem4a 28258 hhxmet 28557 hilxmet 28577 fmcncfil 30493 blssp 34039 lmclim2 34041 geomcau 34042 caures 34043 caushft 34044 sstotbnd2 34060 equivtotbnd 34064 isbndx 34068 isbnd3 34070 ssbnd 34074 totbndbnd 34075 prdstotbnd 34080 prdsbnd2 34081 heibor1lem 34095 heibor1 34096 heiborlem3 34099 heiborlem6 34102 heiborlem8 34104 heiborlem9 34105 heiborlem10 34106 heibor 34107 bfplem1 34108 bfplem2 34109 rrncmslem 34118 ismrer1 34124 reheibor 34125 metpsmet 40027 qndenserrnbllem 41257 qndenserrnbl 41258 qndenserrnopnlem 41260 rrndsxmet 41266 hoiqssbllem2 41583 hoiqssbl 41585 opnvonmbllem2 41593 |
Copyright terms: Public domain | W3C validator |