Metamath Proof Explorer

Theorem pstmxmet

Description: The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis pstmval.1 ⊢ ∼ = ( ~Met ‘ 𝐷 )
Assertion pstmxmet ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ∼ ) ) )

Proof

Step Hyp Ref Expression
1 pstmval.1 ⊢ ∼ = ( ~Met ‘ 𝐷 )
2 eqid ⊢ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) = ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 ab2rexex ⊢ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ∈ V
6 5 uniex ⊢ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ∈ V
7 2 6 fnmpoi ⊢ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) Fn ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) )
8 1 pstmval ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) = ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) )
9 8 fneq1d ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( pstoMet ‘ 𝐷 ) Fn ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ↔ ( 𝑥 ∈ ( 𝑋 / ∼ ) , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝑥 ∃ 𝑏 ∈ 𝑦 𝑧 = ( 𝑎 𝐷 𝑏 ) } ) Fn ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ) )
10 7 9 mpbiri ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) Fn ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) )
11 simpllr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → 𝑥 = [ 𝑎 ] ∼ )
12 simpr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → 𝑦 = [ 𝑏 ] ∼ )
13 11 12 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) )
14 simp-5l ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
15 simp-4r ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → 𝑎 ∈ 𝑋 )
16 simplr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → 𝑏 ∈ 𝑋 )
17 1 pstmfval ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = ( 𝑎 𝐷 𝑏 ) )
18 14 15 16 17 syl3anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = ( 𝑎 𝐷 𝑏 ) )
19 13 18 eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( 𝑎 𝐷 𝑏 ) )
20 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
21 14 20 syl ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
22 21 15 16 fovcdmd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑎 𝐷 𝑏 ) ∈ ℝ* )
23 19 22 eqeltrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
24 elqsi ⊢ ( 𝑦 ∈ ( 𝑋 / ∼ ) → ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ∼ )
25 24 ad2antll ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) → ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ∼ )
26 25 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) → ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ∼ )
27 23 26 r19.29a ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
28 elqsi ⊢ ( 𝑥 ∈ ( 𝑋 / ∼ ) → ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ∼ )
29 28 ad2antrl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) → ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ∼ )
30 27 29 r19.29a ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
31 30 ralrimivva ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ ( 𝑋 / ∼ ) ∀ 𝑦 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* )
32 ffnov ⊢ ( ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ⟶ ℝ* ↔ ( ( pstoMet ‘ 𝐷 ) Fn ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 / ∼ ) ∀ 𝑦 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ∈ ℝ* ) )
33 10 31 32 sylanbrc ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ⟶ ℝ* )
34 17 3expa ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = ( 𝑎 𝐷 𝑏 ) )
35 34 eqeq1d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = 0 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
36 1 breqi ⊢ ( 𝑎 ∼ 𝑏 ↔ 𝑎 ( ~Met ‘ 𝐷 ) 𝑏 )
37 metidv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ( ~Met ‘ 𝐷 ) 𝑏 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
38 37 anassrs ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 ( ~Met ‘ 𝐷 ) 𝑏 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
39 36 38 bitrid ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 ∼ 𝑏 ↔ ( 𝑎 𝐷 𝑏 ) = 0 ) )
40 metider ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) Er 𝑋 )
41 40 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( ~Met ‘ 𝐷 ) Er 𝑋 )
42 ereq1 ⊢ ( ∼ = ( ~Met ‘ 𝐷 ) → ( ∼ Er 𝑋 ↔ ( ~Met ‘ 𝐷 ) Er 𝑋 ) )
43 1 42 ax-mp ⊢ ( ∼ Er 𝑋 ↔ ( ~Met ‘ 𝐷 ) Er 𝑋 )
44 41 43 sylibr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ∼ Er 𝑋 )
45 simplr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → 𝑎 ∈ 𝑋 )
46 44 45 erth ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 ∼ 𝑏 ↔ [ 𝑎 ] ∼ = [ 𝑏 ] ∼ ) )
47 35 39 46 3bitr2d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = 0 ↔ [ 𝑎 ] ∼ = [ 𝑏 ] ∼ ) )
48 47 adantllr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑏 ∈ 𝑋 ) → ( ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = 0 ↔ [ 𝑎 ] ∼ = [ 𝑏 ] ∼ ) )
49 48 adantlr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) → ( ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = 0 ↔ [ 𝑎 ] ∼ = [ 𝑏 ] ∼ ) )
50 49 adantr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = 0 ↔ [ 𝑎 ] ∼ = [ 𝑏 ] ∼ ) )
51 13 eqeq1d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = 0 ) )
52 11 12 eqeq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑥 = 𝑦 ↔ [ 𝑎 ] ∼ = [ 𝑏 ] ∼ ) )
53 50 51 52 3bitr4d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
54 53 26 r19.29a ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
55 54 29 r19.29a ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) → ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
56 simp-6l ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
57 simplr ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝑐 ∈ 𝑋 )
58 simp-6r ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝑎 ∈ 𝑋 )
59 simp-4r ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝑏 ∈ 𝑋 )
60 psmettri2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
61 56 57 58 59 60 syl13anc ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
62 simp-5r ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝑥 = [ 𝑎 ] ∼ )
63 simpllr ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝑦 = [ 𝑏 ] ∼ )
64 62 63 oveq12d ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) )
65 56 58 59 17 syl3anc ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( [ 𝑎 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = ( 𝑎 𝐷 𝑏 ) )
66 64 65 eqtrd ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( 𝑎 𝐷 𝑏 ) )
67 simpr ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → 𝑧 = [ 𝑐 ] ∼ )
68 67 62 oveq12d ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) = ( [ 𝑐 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑎 ] ∼ ) )
69 1 pstmfval ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ( [ 𝑐 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑎 ] ∼ ) = ( 𝑐 𝐷 𝑎 ) )
70 56 57 58 69 syl3anc ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( [ 𝑐 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑎 ] ∼ ) = ( 𝑐 𝐷 𝑎 ) )
71 68 70 eqtrd ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) = ( 𝑐 𝐷 𝑎 ) )
72 67 63 oveq12d ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( [ 𝑐 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) )
73 1 pstmfval ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( [ 𝑐 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = ( 𝑐 𝐷 𝑏 ) )
74 56 57 59 73 syl3anc ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( [ 𝑐 ] ∼ ( pstoMet ‘ 𝐷 ) [ 𝑏 ] ∼ ) = ( 𝑐 𝐷 𝑏 ) )
75 72 74 eqtrd ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) = ( 𝑐 𝐷 𝑏 ) )
76 71 75 oveq12d ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) = ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) )
77 61 66 76 3brtr4d ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
78 77 adantl6r ⊢ ( ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) ∧ 𝑐 ∈ 𝑋 ) ∧ 𝑧 = [ 𝑐 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
79 elqsi ⊢ ( 𝑧 ∈ ( 𝑋 / ∼ ) → ∃ 𝑐 ∈ 𝑋 𝑧 = [ 𝑐 ] ∼ )
80 79 ad5antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ∃ 𝑐 ∈ 𝑋 𝑧 = [ 𝑐 ] ∼ )
81 78 80 r19.29a ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
82 81 adantl5r ⊢ ( ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑦 = [ 𝑏 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
83 24 ad4antlr ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) → ∃ 𝑏 ∈ 𝑋 𝑦 = [ 𝑏 ] ∼ )
84 82 83 r19.29a ⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
85 84 adantl4r ⊢ ( ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ 𝑥 = [ 𝑎 ] ∼ ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
86 28 ad3antlr ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) → ∃ 𝑎 ∈ 𝑋 𝑥 = [ 𝑎 ] ∼ )
87 85 86 r19.29a ⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑧 ∈ ( 𝑋 / ∼ ) ) → ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
88 87 ralrimiva ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) → ∀ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
89 88 anasss ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) → ∀ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) )
90 55 89 jca ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑋 / ∼ ) ∧ 𝑦 ∈ ( 𝑋 / ∼ ) ) ) → ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) )
91 90 ralrimivva ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ ( 𝑋 / ∼ ) ∀ 𝑦 ∈ ( 𝑋 / ∼ ) ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) )
92 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
93 qsexg ⊢ ( 𝑋 ∈ V → ( 𝑋 / ∼ ) ∈ V )
94 isxmet ⊢ ( ( 𝑋 / ∼ ) ∈ V → ( ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ∼ ) ) ↔ ( ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ ( 𝑋 / ∼ ) ∀ 𝑦 ∈ ( 𝑋 / ∼ ) ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) ) ) )
95 92 93 94 3syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ∼ ) ) ↔ ( ( pstoMet ‘ 𝐷 ) : ( ( 𝑋 / ∼ ) × ( 𝑋 / ∼ ) ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ ( 𝑋 / ∼ ) ∀ 𝑦 ∈ ( 𝑋 / ∼ ) ( ( ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑥 ( pstoMet ‘ 𝐷 ) 𝑦 ) ≤ ( ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑥 ) +𝑒 ( 𝑧 ( pstoMet ‘ 𝐷 ) 𝑦 ) ) ) ) ) )
96 33 91 95 mpbir2and ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( pstoMet ‘ 𝐷 ) ∈ ( ∞Met ‘ ( 𝑋 / ∼ ) ) )