This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐷 ) ( 𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ ( 𝑉 “ { 𝑃 } ) ) )