Definition df-metid

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

	Ref	Expression
Assertion	df-metid	⊢ ~Met = ( 𝑑 ∈ ∪ ran PsMet ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmetid	⊢ ~Met
1		vd	⊢ 𝑑
2		cpsmet	⊢ PsMet
3	2	crn	⊢ ran PsMet
4	3	cuni	⊢ ∪ ran PsMet
5		vx	⊢ 𝑥
6		vy	⊢ 𝑦
7	5	cv	⊢ 𝑥
8	1	cv	⊢ 𝑑
9	8	cdm	⊢ dom 𝑑
10	9	cdm	⊢ dom dom 𝑑
11	7 10	wcel	⊢ 𝑥 ∈ dom dom 𝑑
12	6	cv	⊢ 𝑦
13	12 10	wcel	⊢ 𝑦 ∈ dom dom 𝑑
14	11 13	wa	⊢ ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 )
15	7 12 8	co	⊢ ( 𝑥 𝑑 𝑦 )
16		cc0	⊢ 0
17	15 16	wceq	⊢ ( 𝑥 𝑑 𝑦 ) = 0
18	14 17	wa	⊢ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 )
19	18 5 6	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) }
20	1 4 19	cmpt	⊢ ( 𝑑 ∈ ∪ ran PsMet ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } )
21	0 20	wceq	⊢ ~Met = ( 𝑑 ∈ ∪ ran PsMet ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } )