Metamath Proof Explorer


Theorem xmetdmdm

Description: Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion xmetdmdm ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )

Proof

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 𝐷 )