Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  bdbl Unicode version

Theorem bdbl 12850
 Description: The standard bounded metric corresponding to generates the same balls as for radii less than . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
Hypothesis
Ref Expression
stdbdmet.1 inf
Assertion
Ref Expression
bdbl
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem bdbl
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr2 989 . . . . . 6
21adantr 274 . . . . 5
3 simpl1 985 . . . . . . 7
43adantr 274 . . . . . 6
5 simpr1 988 . . . . . . 7
65adantr 274 . . . . . 6
7 simpr 109 . . . . . 6
8 xmetcl 12699 . . . . . 6
94, 6, 7, 8syl3anc 1217 . . . . 5
10 simpll2 1022 . . . . 5
11 xrminltinf 11146 . . . . 5 inf
122, 9, 10, 11syl3anc 1217 . . . 4 inf
13 xmetf 12697 . . . . . . . . 9
14133ad2ant1 1003 . . . . . . . 8
1514adantr 274 . . . . . . 7
1615adantr 274 . . . . . 6
17 stdbdmet.1 . . . . . . 7 inf
1817bdmetval 12847 . . . . . 6 inf
1916, 10, 6, 7, 18syl22anc 1218 . . . . 5 inf
2019breq1d 3971 . . . 4 inf
21 simpr3 990 . . . . . . . 8
22 simpl2 986 . . . . . . . . 9
23 xrlenlt 7921 . . . . . . . . 9
241, 22, 23syl2anc 409 . . . . . . . 8
2521, 24mpbid 146 . . . . . . 7
26 biorf 734 . . . . . . 7
2725, 26syl 14 . . . . . 6
28 orcom 718 . . . . . 6
2927, 28bitrdi 195 . . . . 5
3029adantr 274 . . . 4
3112, 20, 303bitr4d 219 . . 3
3231rabbidva 2697 . 2
3317bdxmet 12848 . . . 4