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