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

Theorem stdbdbl 21312
 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 1037 . . . . . 6
2 simpr1 1003 . . . . . . 7
32adantr 463 . . . . . 6
4 simpr 459 . . . . . 6
5 stdbdmet.1 . . . . . . 7
65stdbdmetval 21309 . . . . . 6
71, 3, 4, 6syl3anc 1230 . . . . 5
87breq1d 4405 . . . 4
9 simplr3 1041 . . . . . . . 8
109biantrud 505 . . . . . . 7
11 simpr2 1004 . . . . . . . . 9
1211adantr 463 . . . . . . . 8
13 simpl1 1000 . . . . . . . . . 10
1413adantr 463 . . . . . . . . 9
15 xmetcl 21126 . . . . . . . . 9
1614, 3, 4, 15syl3anc 1230 . . . . . . . 8
17 xrlemin 11438 . . . . . . . 8
1812, 16, 1, 17syl3anc 1230 . . . . . . 7
1910, 18bitr4d 256 . . . . . 6
2019notbid 292 . . . . 5
21 xrltnle 9683 . . . . . 6
2216, 12, 21syl2anc 659 . . . . 5
2316, 1ifcld 3928 . . . . . 6
24 xrltnle 9683 . . . . . 6
2523, 12, 24syl2anc 659 . . . . 5
2620, 22, 253bitr4d 285 . . . 4
278, 26bitr4d 256 . . 3
2827rabbidva 3050 . 2
295stdbdxmet 21310 . . . 4