Theorem blfvalps 23536

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.

Step	Hyp	Ref	Expression
1		df-bl 20592	. 2 ⊢ ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}))
2		dmeq 5812	. . . . 5 ⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
3	2	dmeqd 5814	. . . 4 ⊢ (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷)
4		psmetdmdm 23458	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷)
5	4	eqcomd 2744	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → dom dom 𝐷 = 𝑋)
6	3, 5	sylan9eqr 2800	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋)
7		eqidd 2739	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ℝ* = ℝ*)
8		simpr 485	. . . . . 6 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
9	8	oveqd 7292	. . . . 5 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥𝑑𝑦) = (𝑥𝐷𝑦))
10	9	breq1d 5084	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑥𝑑𝑦) < 𝑟 ↔ (𝑥𝐷𝑦) < 𝑟))
11	6, 10	rabeqbidv 3420	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟} = {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})
12	6, 7, 11	mpoeq123dv 7350	. 2 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑥 ∈ dom dom 𝑑, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}))
13		elex 3450	. 2 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ V)
14		ssrab2 4013	. . . . . 6 ⊢ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋
15		elfvdm 6806	. . . . . . . 8 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet)
16	15	adantr 481	. . . . . . 7 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → 𝑋 ∈ dom PsMet)
17		elpw2g 5268	. . . . . . 7 ⊢ (𝑋 ∈ dom PsMet → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋))
18	16, 17	syl 17	. . . . . 6 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → ({𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ⊆ 𝑋))
19	14, 18	mpbiri 257	. . . . 5 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*)) → {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋)
20	19	ralrimivva 3123	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ* {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋)
21		eqid 2738	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})
22	21	fmpo 7908	. . . 4 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ* {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟} ∈ 𝒫 𝑋 ↔ (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 × ℝ*)⟶𝒫 𝑋)
23	20, 22	sylib 217	. . 3 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 × ℝ*)⟶𝒫 𝑋)
24		xrex 12727	. . . 4 ⊢ ℝ* ∈ V
25		xpexg 7600	. . . 4 ⊢ ((𝑋 ∈ dom PsMet ∧ ℝ* ∈ V) → (𝑋 × ℝ*) ∈ V)
26	15, 24, 25	sylancl 586	. . 3 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑋 × ℝ*) ∈ V)
27	15	pwexd 5302	. . 3 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝒫 𝑋 ∈ V)
28		fex2 7780	. . 3 ⊢ (((𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}):(𝑋 × ℝ*)⟶𝒫 𝑋 ∧ (𝑋 × ℝ*) ∈ V ∧ 𝒫 𝑋 ∈ V) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V)
29	23, 26, 27, 28	syl3anc 1370	. 2 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}) ∈ V)
30	1, 12, 13, 29	fvmptd2 6883	1 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟}))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  {crab 3068  Vcvv 3432   ⊆ wss 3887  𝒫 cpw 4533   class class class wbr 5074   × cxp 5587  dom cdm 5589  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277  ℝ^*cxr 11008   < clt 11009  PsMetcpsmet 20581  ballcbl 20584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-map 8617  df-xr 11013  df-psmet 20589  df-bl 20592

This theorem is referenced by:  blfval  23537  blvalps  23538  blfps  23559