Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  stdbdbl Structured version   Unicode version

Theorem stdbdbl 18539
 Description: The standard bounded metric corresponding to generates the same balls as for radii less than . (Contributed by Mario Carneiro, 26-Aug-2015.)
Hypothesis
Ref Expression
stdbdmet.1
Assertion
Ref Expression
stdbdbl
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem stdbdbl
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpll2 997 . . . . . 6
2 simpr1 963 . . . . . . 7
32adantr 452 . . . . . 6
4 simpr 448 . . . . . 6
5 stdbdmet.1 . . . . . . 7
65stdbdmetval 18536 . . . . . 6
71, 3, 4, 6syl3anc 1184 . . . . 5
87breq1d 4214 . . . 4
9 simplr3 1001 . . . . . . . 8
109biantrud 494 . . . . . . 7
11 simpr2 964 . . . . . . . . 9
1211adantr 452 . . . . . . . 8
13 simpl1 960 . . . . . . . . . 10
1413adantr 452 . . . . . . . . 9
15 xmetcl 18353 . . . . . . . . 9
1614, 3, 4, 15syl3anc 1184 . . . . . . . 8
17 xrlemin 10764 . . . . . . . 8
1812, 16, 1, 17syl3anc 1184 . . . . . . 7
1910, 18bitr4d 248 . . . . . 6
2019notbid 286 . . . . 5
21 xrltnle 9136 . . . . . 6
2216, 12, 21syl2anc 643 . . . . 5
23 ifcl 3767 . . . . . . 7
2416, 1, 23syl2anc 643 . . . . . 6
25 xrltnle 9136 . . . . . 6
2624, 12, 25syl2anc 643 . . . . 5
2720, 22, 263bitr4d 277 . . . 4
288, 27bitr4d 248 . . 3
2928rabbidva 2939 . 2
305stdbdxmet 18537 . . . 4