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 ‘ ( 𝑋 / ∼ ) ) )