ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isxmet GIF version

Theorem isxmet 13396
Description: Express the predicate "𝐷 is an extended metric". (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
isxmet (𝑋𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐷   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧)

Proof of Theorem isxmet
Dummy variables 𝑑 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2746 . . . . 5 (𝑋𝐴𝑋 ∈ V)
2 fnmap 6645 . . . . . . . 8 𝑚 Fn (V × V)
3 xrex 9825 . . . . . . . 8 * ∈ V
4 sqxpexg 4736 . . . . . . . 8 (𝑋 ∈ V → (𝑋 × 𝑋) ∈ V)
5 fnovex 5898 . . . . . . . 8 (( ↑𝑚 Fn (V × V) ∧ ℝ* ∈ V ∧ (𝑋 × 𝑋) ∈ V) → (ℝ*𝑚 (𝑋 × 𝑋)) ∈ V)
62, 3, 4, 5mp3an12i 1341 . . . . . . 7 (𝑋 ∈ V → (ℝ*𝑚 (𝑋 × 𝑋)) ∈ V)
7 rabexg 4141 . . . . . . 7 ((ℝ*𝑚 (𝑋 × 𝑋)) ∈ V → {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))} ∈ V)
86, 7syl 14 . . . . . 6 (𝑋 ∈ V → {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))} ∈ V)
9 xpeq12 4639 . . . . . . . . . 10 ((𝑡 = 𝑋𝑡 = 𝑋) → (𝑡 × 𝑡) = (𝑋 × 𝑋))
109anidms 397 . . . . . . . . 9 (𝑡 = 𝑋 → (𝑡 × 𝑡) = (𝑋 × 𝑋))
1110oveq2d 5881 . . . . . . . 8 (𝑡 = 𝑋 → (ℝ*𝑚 (𝑡 × 𝑡)) = (ℝ*𝑚 (𝑋 × 𝑋)))
12 raleq 2670 . . . . . . . . . . 11 (𝑡 = 𝑋 → (∀𝑧𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)) ↔ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦))))
1312anbi2d 464 . . . . . . . . . 10 (𝑡 = 𝑋 → ((((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦))) ↔ (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))))
1413raleqbi1dv 2678 . . . . . . . . 9 (𝑡 = 𝑋 → (∀𝑦𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦))) ↔ ∀𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))))
1514raleqbi1dv 2678 . . . . . . . 8 (𝑡 = 𝑋 → (∀𝑥𝑡𝑦𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦))) ↔ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))))
1611, 15rabeqbidv 2730 . . . . . . 7 (𝑡 = 𝑋 → {𝑑 ∈ (ℝ*𝑚 (𝑡 × 𝑡)) ∣ ∀𝑥𝑡𝑦𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))} = {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))})
17 df-xmet 13039 . . . . . . 7 ∞Met = (𝑡 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑡 × 𝑡)) ∣ ∀𝑥𝑡𝑦𝑡 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑡 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))})
1816, 17fvmptg 5584 . . . . . 6 ((𝑋 ∈ V ∧ {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))} ∈ V) → (∞Met‘𝑋) = {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))})
198, 18mpdan 421 . . . . 5 (𝑋 ∈ V → (∞Met‘𝑋) = {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))})
201, 19syl 14 . . . 4 (𝑋𝐴 → (∞Met‘𝑋) = {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))})
2120eleq2d 2245 . . 3 (𝑋𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ 𝐷 ∈ {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))}))
22 oveq 5871 . . . . . . . 8 (𝑑 = 𝐷 → (𝑥𝑑𝑦) = (𝑥𝐷𝑦))
2322eqeq1d 2184 . . . . . . 7 (𝑑 = 𝐷 → ((𝑥𝑑𝑦) = 0 ↔ (𝑥𝐷𝑦) = 0))
2423bibi1d 233 . . . . . 6 (𝑑 = 𝐷 → (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ↔ ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)))
25 oveq 5871 . . . . . . . . 9 (𝑑 = 𝐷 → (𝑧𝑑𝑥) = (𝑧𝐷𝑥))
26 oveq 5871 . . . . . . . . 9 (𝑑 = 𝐷 → (𝑧𝑑𝑦) = (𝑧𝐷𝑦))
2725, 26oveq12d 5883 . . . . . . . 8 (𝑑 = 𝐷 → ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)) = ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
2822, 27breq12d 4011 . . . . . . 7 (𝑑 = 𝐷 → ((𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)) ↔ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
2928ralbidv 2475 . . . . . 6 (𝑑 = 𝐷 → (∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)) ↔ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
3024, 29anbi12d 473 . . . . 5 (𝑑 = 𝐷 → ((((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦))) ↔ (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))
31302ralbidv 2499 . . . 4 (𝑑 = 𝐷 → (∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦))) ↔ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))
3231elrab 2891 . . 3 (𝐷 ∈ {𝑑 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∣ ∀𝑥𝑋𝑦𝑋 (((𝑥𝑑𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝑑𝑦) ≤ ((𝑧𝑑𝑥) +𝑒 (𝑧𝑑𝑦)))} ↔ (𝐷 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))
3321, 32bitrdi 196 . 2 (𝑋𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
34 sqxpexg 4736 . . . 4 (𝑋𝐴 → (𝑋 × 𝑋) ∈ V)
35 elmapg 6651 . . . 4 ((ℝ* ∈ V ∧ (𝑋 × 𝑋) ∈ V) → (𝐷 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ↔ 𝐷:(𝑋 × 𝑋)⟶ℝ*))
363, 34, 35sylancr 414 . . 3 (𝑋𝐴 → (𝐷 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ↔ 𝐷:(𝑋 × 𝑋)⟶ℝ*))
3736anbi1d 465 . 2 (𝑋𝐴 → ((𝐷 ∈ (ℝ*𝑚 (𝑋 × 𝑋)) ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
3833, 37bitrd 188 1 (𝑋𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥𝑋𝑦𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2146  wral 2453  {crab 2457  Vcvv 2735   class class class wbr 3998   × cxp 4618   Fn wfn 5203  wf 5204  cfv 5208  (class class class)co 5865  𝑚 cmap 6638  0cc0 7786  *cxr 7965  cle 7967   +𝑒 cxad 9739  ∞Metcxmet 13031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-cnex 7877  ax-resscn 7878
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-fv 5216  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-map 6640  df-pnf 7968  df-mnf 7969  df-xr 7970  df-xmet 13039
This theorem is referenced by:  isxmetd  13398  xmetf  13401  ismet2  13405  xmeteq0  13410  xmettri2  13412
  Copyright terms: Public domain W3C validator