Theorem metustbl

Description: The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017)

	Ref	Expression
Assertion	metustbl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑎 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ ( 𝑉 “ { 𝑃 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2		simp3	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
3		simpr	⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) ) ∧ 𝑤 ⊆ 𝑉 ) → 𝑤 ⊆ 𝑉 )
4		eqid	⊢ ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) = ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) )
5	4	elrnmpt	⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) ↔ ∃ 𝑟 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) )
6	5	elv	⊢ ( 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) ↔ ∃ 𝑟 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) )
7	6	biimpi	⊢ ( 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) → ∃ 𝑟 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) )
8	7	ad2antlr	⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) ) ∧ 𝑤 ⊆ 𝑉 ) → ∃ 𝑟 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) )
9		sseq1	⊢ ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) → ( 𝑤 ⊆ 𝑉 ↔ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 ) )
10	9	biimpcd	⊢ ( 𝑤 ⊆ 𝑉 → ( 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) → ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 ) )
11	10	reximdv	⊢ ( 𝑤 ⊆ 𝑉 → ( ∃ 𝑟 ∈ ℝ+ 𝑤 = ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) → ∃ 𝑟 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 ) )
12	3 8 11	sylc	⊢ ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) ) ∧ 𝑤 ⊆ 𝑉 ) → ∃ 𝑟 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 )
13	2	ne0d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑋 ≠ ∅ )
14		simp2	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑉 ∈ ( metUnif ‘ 𝐷 ) )
15		metuel	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) 𝑤 ⊆ 𝑉 ) ) )
16	15	simplbda	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ) → ∃ 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) 𝑤 ⊆ 𝑉 )
17	13 1 14 16	syl21anc	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑤 ∈ ran ( 𝑟 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ) 𝑤 ⊆ 𝑉 )
18	12 17	r19.29a	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑟 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 )
19		imass1	⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 → ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) “ { 𝑃 } ) ⊆ ( 𝑉 “ { 𝑃 } ) )
20	19	reximi	⊢ ( ∃ 𝑟 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 → ∃ 𝑟 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) “ { 𝑃 } ) ⊆ ( 𝑉 “ { 𝑃 } ) )
21		blval2	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) “ { 𝑃 } ) )
22	21	sseq1d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) “ { 𝑃 } ) ⊆ ( 𝑉 “ { 𝑃 } ) ) )
23	22	3expa	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) “ { 𝑃 } ) ⊆ ( 𝑉 “ { 𝑃 } ) ) )
24	23	rexbidva	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) ↔ ∃ 𝑟 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) “ { 𝑃 } ) ⊆ ( 𝑉 “ { 𝑃 } ) ) )
25	20 24	imbitrrid	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) ) )
26	25	imp	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∃ 𝑟 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑟 ) ) ⊆ 𝑉 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) )
27	1 2 18 26	syl21anc	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) )
28		blssexps	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑎 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ ( 𝑉 “ { 𝑃 } ) ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) ) )
29	28	3adant2	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑎 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ ( 𝑉 “ { 𝑃 } ) ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑉 “ { 𝑃 } ) ) )
30	27 29	mpbird	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑉 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑎 ∈ ran ( ball ‘ 𝐷 ) ( 𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ ( 𝑉 “ { 𝑃 } ) ) )