Theorem metidval

Description: Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Assertion	metidval	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )

Proof

Step	Hyp	Ref	Expression
1		df-metid	⊢ ~Met = ( 𝑑 ∈ ∪ ran PsMet ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } )
2	1	a1i	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ~Met = ( 𝑑 ∈ ∪ ran PsMet ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } ) )
3		simpr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
4	3	dmeqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom 𝑑 = dom 𝐷 )
5	4	dmeqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = dom dom 𝐷 )
6		psmetdmdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
7	6	adantr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝐷 )
8	5 7	eqtr4d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
9	8	eleq2d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ dom dom 𝑑 ↔ 𝑥 ∈ 𝑋 ) )
10	8	eleq2d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ∈ dom dom 𝑑 ↔ 𝑦 ∈ 𝑋 ) )
11	9 10	anbi12d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
12	3	oveqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
13	12	eqeq1d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 𝑑 𝑦 ) = 0 ↔ ( 𝑥 𝐷 𝑦 ) = 0 ) )
14	11 13	anbi12d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ) )
15	14	opabbidv	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑 ) ∧ ( 𝑥 𝑑 𝑦 ) = 0 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )
16		elfvdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ dom PsMet )
17		fveq2	⊢ ( 𝑥 = 𝑋 → ( PsMet ‘ 𝑥 ) = ( PsMet ‘ 𝑋 ) )
18	17	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐷 ∈ ( PsMet ‘ 𝑥 ) ↔ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) )
19	18	rspcev	⊢ ( ( 𝑋 ∈ dom PsMet ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
20	16 19	mpancom	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
21		df-psmet	⊢ PsMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 𝑑 𝑦 ) = 0 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } )
22	21	funmpt2	⊢ Fun PsMet
23		elunirn	⊢ ( Fun PsMet → ( 𝐷 ∈ ∪ ran PsMet ↔ ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) ) )
24	22 23	ax-mp	⊢ ( 𝐷 ∈ ∪ ran PsMet ↔ ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
25	20 24	sylibr	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ ∪ ran PsMet )
26		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ⊆ ( 𝑋 × 𝑋 )
27		elfvex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
28	27 27	xpexd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ V )
29		ssexg	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ⊆ ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ∈ V )
30	26 28 29	sylancr	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ∈ V )
31	2 15 25 30	fvmptd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )