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

Theorem blfvalps 12613
 Description: The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Assertion
Ref Expression
blfvalps (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}))
Distinct variable groups:   𝑥,𝑟,𝑦,𝐷   𝑋,𝑟,𝑥,𝑦

Proof of Theorem blfvalps
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 df-bl 12218 . . 3 ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}))
21a1i 9 . 2 (𝐷 ∈ (PsMet‘𝑋) → ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟})))
3 dmeq 4748 . . . . 5 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
43dmeqd 4750 . . . 4 (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷)
5 psmetdmdm 12552 . . . . 5 (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷)
65eqcomd 2146 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → dom dom 𝐷 = 𝑋)
74, 6sylan9eqr 2195 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋)
8 eqidd 2141 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ℝ* = ℝ*)
9 simpr 109 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
109oveqd 5800 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦))
1110breq1d 3948 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) < 𝑟 ↔ (𝑥𝐷𝑦) < 𝑟))
127, 11rabeqbidv 2685 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟} = {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})
137, 8, 12mpoeq123dv 5842 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}) = (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}))
14 elex 2701 . 2 (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V)
15 ssrab2 3188 . . . . . 6 {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋
16 psmetrel 12550 . . . . . . . . 9 Rel PsMet
17 relelfvdm 5462 . . . . . . . . 9 ((Rel PsMet ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝑋 ∈ dom PsMet)
1816, 17mpan 421 . . . . . . . 8 (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet)
1918adantr 274 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥𝑋𝑟 ∈ ℝ*)) → 𝑋 ∈ dom PsMet)
20 elpw2g 4090 . . . . . . 7 (𝑋 ∈ dom PsMet → ({𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋))
2119, 20syl 14 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥𝑋𝑟 ∈ ℝ*)) → ({𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋))
2215, 21mpbiri 167 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥𝑋𝑟 ∈ ℝ*)) → {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋)
2322ralrimivva 2518 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥𝑋𝑟 ∈ ℝ* {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋)
24 eqid 2140 . . . . 5 (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) = (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})
2524fmpo 6108 . . . 4 (∀𝑥𝑋𝑟 ∈ ℝ* {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 × ℝ*)⟶𝒫 𝑋)
2623, 25sylib 121 . . 3 (𝐷 ∈ (PsMet‘𝑋) → (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 × ℝ*)⟶𝒫 𝑋)
27 xrex 9689 . . . 4 * ∈ V
28 xpexg 4662 . . . 4 ((𝑋 ∈ dom PsMet ∧ ℝ* ∈ V) → (𝑋 × ℝ*) ∈ V)
2918, 27, 28sylancl 410 . . 3 (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × ℝ*) ∈ V)
3018pwexd 4114 . . 3 (𝐷 ∈ (PsMet‘𝑋) → 𝒫 𝑋 ∈ V)
31 fex2 5300 . . 3 (((𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 × ℝ*)⟶𝒫 𝑋 ∧ (𝑋 × ℝ*) ∈ V ∧ 𝒫 𝑋 ∈ V) → (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V)
3226, 29, 30, 31syl3anc 1217 . 2 (𝐷 ∈ (PsMet‘𝑋) → (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V)
332, 13, 14, 32fvmptd 5511 1 (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥𝑋, 𝑟 ∈ ℝ* ↦ {𝑦𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ∀wral 2417  {crab 2421  Vcvv 2690   ⊆ wss 3077  𝒫 cpw 3516   class class class wbr 3938   ↦ cmpt 3998   × cxp 4546  dom cdm 4548  Rel wrel 4553  ⟶wf 5128  ‘cfv 5132  (class class class)co 5783   ∈ cmpo 5785  ℝ*cxr 7843   < clt 7844  PsMetcpsmet 12207  ballcbl 12210 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-cnex 7755  ax-resscn 7756 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-fv 5140  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-map 6553  df-pnf 7846  df-mnf 7847  df-xr 7848  df-psmet 12215  df-bl 12218 This theorem is referenced by:  blfval  12614  blvalps  12616  blfps  12637
 Copyright terms: Public domain W3C validator