Metamath Proof Explorer

Theorem ismet

Description: Express the predicate " D is a metric." (Contributed by NM, 25-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ismet ⊢X∈A→D∈Met⁡X↔D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy

Proof

Step Hyp Ref Expression
1 elex ⊢X∈A→X∈V
2 xpeq12 ⊢t=X∧t=X→t×t=X×X
3 2 anidms ⊢t=X→t×t=X×X
4 3 oveq2d ⊢t=X→ℝt×t=ℝX×X
5 raleq ⊢t=X→∀z∈txdy≤zdx+zdy↔∀z∈Xxdy≤zdx+zdy
6 5 anbi2d ⊢t=X→xdy=0↔x=y∧∀z∈txdy≤zdx+zdy↔xdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
7 6 raleqbi1dv ⊢t=X→∀y∈txdy=0↔x=y∧∀z∈txdy≤zdx+zdy↔∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
8 7 raleqbi1dv ⊢t=X→∀x∈t∀y∈txdy=0↔x=y∧∀z∈txdy≤zdx+zdy↔∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
9 4 8 rabeqbidv ⊢t=X→d∈ℝt×t|∀x∈t∀y∈txdy=0↔x=y∧∀z∈txdy≤zdx+zdy=d∈ℝX×X|∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
10 df-met ⊢Met=t∈V⟼d∈ℝt×t|∀x∈t∀y∈txdy=0↔x=y∧∀z∈txdy≤zdx+zdy
11 ovex ⊢ℝX×X∈V
12 11 rabex ⊢d∈ℝX×X|∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy∈V
13 9 10 12 fvmpt ⊢X∈V→Met⁡X=d∈ℝX×X|∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
14 1 13 syl ⊢X∈A→Met⁡X=d∈ℝX×X|∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
15 14 eleq2d ⊢X∈A→D∈Met⁡X↔D∈d∈ℝX×X|∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy
16 oveq ⊢d=D→xdy=xDy
17 16 eqeq1d ⊢d=D→xdy=0↔xDy=0
18 17 bibi1d ⊢d=D→xdy=0↔x=y↔xDy=0↔x=y
19 oveq ⊢d=D→zdx=zDx
20 oveq ⊢d=D→zdy=zDy
21 19 20 oveq12d ⊢d=D→zdx+zdy=zDx+zDy
22 16 21 breq12d ⊢d=D→xdy≤zdx+zdy↔xDy≤zDx+zDy
23 22 ralbidv ⊢d=D→∀z∈Xxdy≤zdx+zdy↔∀z∈XxDy≤zDx+zDy
24 18 23 anbi12d ⊢d=D→xdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy↔xDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
25 24 2ralbidv ⊢d=D→∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy↔∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
26 25 elrab ⊢D∈d∈ℝX×X|∀x∈X∀y∈Xxdy=0↔x=y∧∀z∈Xxdy≤zdx+zdy↔D∈ℝX×X∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
27 15 26 bitrdi ⊢X∈A→D∈Met⁡X↔D∈ℝX×X∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
28 reex ⊢ℝ∈V
29 sqxpexg ⊢X∈A→X×X∈V
30 elmapg ⊢ℝ∈V∧X×X∈V→D∈ℝX×X↔D:X×X⟶ℝ
31 28 29 30 sylancr ⊢X∈A→D∈ℝX×X↔D:X×X⟶ℝ
32 31 anbi1d ⊢X∈A→D∈ℝX×X∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy↔D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
33 27 32 bitrd ⊢X∈A→D∈Met⁡X↔D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy