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 DPsMetXVmetUnifDPXaranballDPaaVP

Proof

Step Hyp Ref Expression
1 simp1 DPsMetXVmetUnifDPXDPsMetX
2 simp3 DPsMetXVmetUnifDPXPX
3 simpr DPsMetXVmetUnifDPXwranr+D-10rwVwV
4 eqid r+D-10r=r+D-10r
5 4 elrnmpt wVwranr+D-10rr+w=D-10r
6 5 elv wranr+D-10rr+w=D-10r
7 6 biimpi wranr+D-10rr+w=D-10r
8 7 ad2antlr DPsMetXVmetUnifDPXwranr+D-10rwVr+w=D-10r
9 sseq1 w=D-10rwVD-10rV
10 9 biimpcd wVw=D-10rD-10rV
11 10 reximdv wVr+w=D-10rr+D-10rV
12 3 8 11 sylc DPsMetXVmetUnifDPXwranr+D-10rwVr+D-10rV
13 2 ne0d DPsMetXVmetUnifDPXX
14 simp2 DPsMetXVmetUnifDPXVmetUnifD
15 metuel XDPsMetXVmetUnifDVX×Xwranr+D-10rwV
16 15 simplbda XDPsMetXVmetUnifDwranr+D-10rwV
17 13 1 14 16 syl21anc DPsMetXVmetUnifDPXwranr+D-10rwV
18 12 17 r19.29a DPsMetXVmetUnifDPXr+D-10rV
19 imass1 D-10rVD-10rPVP
20 19 reximi r+D-10rVr+D-10rPVP
21 blval2 DPsMetXPXr+PballDr=D-10rP
22 21 sseq1d DPsMetXPXr+PballDrVPD-10rPVP
23 22 3expa DPsMetXPXr+PballDrVPD-10rPVP
24 23 rexbidva DPsMetXPXr+PballDrVPr+D-10rPVP
25 20 24 imbitrrid DPsMetXPXr+D-10rVr+PballDrVP
26 25 imp DPsMetXPXr+D-10rVr+PballDrVP
27 1 2 18 26 syl21anc DPsMetXVmetUnifDPXr+PballDrVP
28 blssexps DPsMetXPXaranballDPaaVPr+PballDrVP
29 28 3adant2 DPsMetXVmetUnifDPXaranballDPaaVPr+PballDrVP
30 27 29 mpbird DPsMetXVmetUnifDPXaranballDPaaVP