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 ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y

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 ∈ t x d y ≤ z d x + z d y ↔ ∀ z ∈ X x d y ≤ z d x + z d y
6 5 anbi2d ⊢ t = X → x d y = 0 ↔ x = y ∧ ∀ z ∈ t x d y ≤ z d x + z d y ↔ x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
7 6 raleqbi1dv ⊢ t = X → ∀ y ∈ t x d y = 0 ↔ x = y ∧ ∀ z ∈ t x d y ≤ z d x + z d y ↔ ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
8 7 raleqbi1dv ⊢ t = X → ∀ x ∈ t ∀ y ∈ t x d y = 0 ↔ x = y ∧ ∀ z ∈ t x d y ≤ z d x + z d y ↔ ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
9 4 8 rabeqbidv ⊢ t = X → d ∈ ℝ t × t | ∀ x ∈ t ∀ y ∈ t x d y = 0 ↔ x = y ∧ ∀ z ∈ t x d y ≤ z d x + z d y = d ∈ ℝ X × X | ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
10 df-met ⊢ Met = t ∈ V ⟼ d ∈ ℝ t × t | ∀ x ∈ t ∀ y ∈ t x d y = 0 ↔ x = y ∧ ∀ z ∈ t x d y ≤ z d x + z d y
11 ovex ⊢ ℝ X × X ∈ V
12 11 rabex ⊢ d ∈ ℝ X × X | ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y ∈ V
13 9 10 12 fvmpt ⊢ X ∈ V → Met ⁡ X = d ∈ ℝ X × X | ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
14 1 13 syl ⊢ X ∈ A → Met ⁡ X = d ∈ ℝ X × X | ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
15 14 eleq2d ⊢ X ∈ A → D ∈ Met ⁡ X ↔ D ∈ d ∈ ℝ X × X | ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y
16 oveq ⊢ d = D → x d y = x D y
17 16 eqeq1d ⊢ d = D → x d y = 0 ↔ x D y = 0
18 17 bibi1d ⊢ d = D → x d y = 0 ↔ x = y ↔ x D y = 0 ↔ x = y
19 oveq ⊢ d = D → z d x = z D x
20 oveq ⊢ d = D → z d y = z D y
21 19 20 oveq12d ⊢ d = D → z d x + z d y = z D x + z D y
22 16 21 breq12d ⊢ d = D → x d y ≤ z d x + z d y ↔ x D y ≤ z D x + z D y
23 22 ralbidv ⊢ d = D → ∀ z ∈ X x d y ≤ z d x + z d y ↔ ∀ z ∈ X x D y ≤ z D x + z D y
24 18 23 anbi12d ⊢ d = D → x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y ↔ x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
25 24 2ralbidv ⊢ d = D → ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y ↔ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
26 25 elrab ⊢ D ∈ d ∈ ℝ X × X | ∀ x ∈ X ∀ y ∈ X x d y = 0 ↔ x = y ∧ ∀ z ∈ X x d y ≤ z d x + z d y ↔ D ∈ ℝ X × X ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
27 15 26 bitrdi ⊢ X ∈ A → D ∈ Met ⁡ X ↔ D ∈ ℝ X × X ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
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 ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y ↔ D : X × X ⟶ ℝ ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
33 27 32 bitrd ⊢ X ∈ A → D ∈ Met ⁡ X ↔ D : X × X ⟶ ℝ ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y