![]() |
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 22185 | . 2 ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ)) | |
2 | 1 | simplbi 475 | 1 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 × cxp 5141 ⟶wf 5922 ‘cfv 5926 ℝcr 9973 ∞Metcxmt 19779 Metcme 19780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-mulcl 10036 ax-i2m1 10042 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-mpt 4763 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-er 7787 df-map 7901 df-en 7998 df-dom 7999 df-sdom 8000 df-pnf 10114 df-mnf 10115 df-xr 10116 df-xadd 11985 df-xmet 19787 df-met 19788 |
This theorem is referenced by: metdmdm 22188 meteq0 22191 mettri2 22193 met0 22195 metge0 22197 metsym 22202 metrtri 22209 metgt0 22211 metres2 22215 prdsmet 22222 imasf1omet 22228 blpnf 22249 bl2in 22252 isms2 22302 setsms 22332 tmsms 22339 metss2lem 22363 metss2 22364 methaus 22372 dscopn 22425 ngpocelbl 22555 cnxmet 22623 rexmet 22641 metdcn2 22689 metdsre 22703 metdscn2 22707 lebnumlem1 22807 lebnumlem2 22808 lebnumlem3 22809 lebnum 22810 xlebnum 22811 cmetcaulem 23132 cmetcau 23133 iscmet3lem1 23135 iscmet3lem2 23136 iscmet3 23137 equivcfil 23143 equivcau 23144 cmetss 23159 relcmpcmet 23161 cmpcmet 23162 cncmet 23165 bcthlem2 23168 bcthlem3 23169 bcthlem4 23170 bcthlem5 23171 bcth2 23173 bcth3 23174 cmetcusp1 23195 cmetcusp 23196 minveclem3 23246 imsxmet 27675 blocni 27788 ubthlem1 27854 ubthlem2 27855 minvecolem4a 27861 hhxmet 28160 hilxmet 28180 fmcncfil 30105 blssp 33682 lmclim2 33684 geomcau 33685 caures 33686 caushft 33687 sstotbnd2 33703 equivtotbnd 33707 isbndx 33711 isbnd3 33713 ssbnd 33717 totbndbnd 33718 prdstotbnd 33723 prdsbnd2 33724 heibor1lem 33738 heibor1 33739 heiborlem3 33742 heiborlem6 33745 heiborlem8 33747 heiborlem9 33748 heiborlem10 33749 heibor 33750 bfplem1 33751 bfplem2 33752 rrncmslem 33761 ismrer1 33767 reheibor 33768 metpsmet 39582 qndenserrnbllem 40832 qndenserrnbl 40833 qndenserrnopnlem 40835 rrndsxmet 40841 hoiqssbllem2 41158 hoiqssbl 41160 opnvonmbllem2 41168 |
Copyright terms: Public domain | W3C validator |