Metamath Proof Explorer

Theorem isxmet

Description: Express the predicate " D is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion isxmet ⊢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-xmet ⊢∞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 xrex ⊢ℝ*∈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