Definition df-pstm

Description: Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Assertion	df-pstm	⊢ pstoMet = ( 𝑑 ∈ ∪ ran PsMet ↦ ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpstm	⊢ pstoMet
1		vd	⊢ 𝑑
2		cpsmet	⊢ PsMet
3	2	crn	⊢ ran PsMet
4	3	cuni	⊢ ∪ ran PsMet
5		va	⊢ 𝑎
6	1	cv	⊢ 𝑑
7	6	cdm	⊢ dom 𝑑
8	7	cdm	⊢ dom dom 𝑑
9		cmetid	⊢ ~Met
10	6 9	cfv	⊢ ( ~Met ‘ 𝑑 )
11	8 10	cqs	⊢ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) )
12		vb	⊢ 𝑏
13		vz	⊢ 𝑧
14		vx	⊢ 𝑥
15	5	cv	⊢ 𝑎
16		vy	⊢ 𝑦
17	12	cv	⊢ 𝑏
18	13	cv	⊢ 𝑧
19	14	cv	⊢ 𝑥
20	16	cv	⊢ 𝑦
21	19 20 6	co	⊢ ( 𝑥 𝑑 𝑦 )
22	18 21	wceq	⊢ 𝑧 = ( 𝑥 𝑑 𝑦 )
23	22 16 17	wrex	⊢ ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 )
24	23 14 15	wrex	⊢ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 )
25	24 13	cab	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) }
26	25	cuni	⊢ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) }
27	5 12 11 11 26	cmpo	⊢ ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } )
28	1 4 27	cmpt	⊢ ( 𝑑 ∈ ∪ ran PsMet ↦ ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )
29	0 28	wceq	⊢ pstoMet = ( 𝑑 ∈ ∪ ran PsMet ↦ ( 𝑎 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) , 𝑏 ∈ ( dom dom 𝑑 / ( ~Met ‘ 𝑑 ) ) ↦ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑏 𝑧 = ( 𝑥 𝑑 𝑦 ) } ) )