Theorem tmsbas

Description: The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypothesis	tmsbas.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
Assertion	tmsbas	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
2		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
3	2 1	tmslem	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝐷 = ( dist ‘ 𝐾 ) ∧ ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) ) )
4	3	simp1d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )