Description: Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xmetdmdm | β’ ( π· β ( βMet β π ) β π = dom dom π· ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xmetf | β’ ( π· β ( βMet β π ) β π· : ( π Γ π ) βΆ β* ) | |
2 | 1 | fdmd | β’ ( π· β ( βMet β π ) β dom π· = ( π Γ π ) ) |
3 | 2 | dmeqd | β’ ( π· β ( βMet β π ) β dom dom π· = dom ( π Γ π ) ) |
4 | dmxpid | β’ dom ( π Γ π ) = π | |
5 | 3 4 | eqtr2di | β’ ( π· β ( βMet β π ) β π = dom dom π· ) |