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