Metamath Proof Explorer
Description: A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)
|
|
Ref |
Expression |
|
Assertion |
metxmet |
β’ ( π· β ( Met β π ) β π· β ( βMet β π ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ismet2 |
β’ ( π· β ( Met β π ) β ( π· β ( βMet β π ) β§ π· : ( π Γ π ) βΆ β ) ) |
2 |
1
|
simplbi |
β’ ( π· β ( Met β π ) β π· β ( βMet β π ) ) |