Theorem blfvalps

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)

	Ref	Expression
Assertion	blfvalps	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )

Proof

Step	Hyp	Ref	Expression
1		df-bl	⊢ ball = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑟 } ) )
2		dmeq	⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
3	2	dmeqd	⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
4		psmetdmdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
5	4	eqcomd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom dom 𝐷 = 𝑋 )
6	3 5	sylan9eqr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
7		eqidd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ℝ* = ℝ* )
8		simpr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
9	8	oveqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
10	9	breq1d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 𝑑 𝑦 ) < 𝑟 ↔ ( 𝑥 𝐷 𝑦 ) < 𝑟 ) )
11	6 10	rabeqbidv	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑟 } = { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } )
12	6 7 11	mpoeq123dv	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ dom dom 𝑑 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑟 } ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )
13		elex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ V )
14		ssrab2	⊢ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋
15		elfvdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ dom PsMet )
16	15	adantr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ) → 𝑋 ∈ dom PsMet )
17		elpw2g	⊢ ( 𝑋 ∈ dom PsMet → ( { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 ) )
18	16 17	syl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ) → ( { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 ) )
19	14 18	mpbiri	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 )
20	19	ralrimivva	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ* { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 )
21		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } )
22	21	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ* { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
23	20 22	sylib	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
24		xrex	⊢ ℝ* ∈ V
25		xpexg	⊢ ( ( 𝑋 ∈ dom PsMet ∧ ℝ* ∈ V ) → ( 𝑋 × ℝ* ) ∈ V )
26	15 24 25	sylancl	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑋 × ℝ* ) ∈ V )
27	15	pwexd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝒫 𝑋 ∈ V )
28		fex2	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ∧ ( 𝑋 × ℝ* ) ∈ V ∧ 𝒫 𝑋 ∈ V ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) ∈ V )
29	23 26 27 28	syl3anc	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) ∈ V )
30	1 12 13 29	fvmptd2	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )