This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psmetdmdm

Description: Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetdmdm ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
2 ispsmet ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
3 2 biimpa ⊢ ( ( 𝑋 ∈ V ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
4 1 3 mpancom ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐷 𝑥 ) = 0 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
5 4 simpld ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
6 fdm ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → dom 𝐷 = ( 𝑋 × 𝑋 ) )
7 6 dmeqd ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → dom dom 𝐷 = dom ( 𝑋 × 𝑋 ) )
8 5 7 syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom dom 𝐷 = dom ( 𝑋 × 𝑋 ) )
9 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
10 8 9 eqtr2di ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )