Metamath Proof Explorer


Theorem isbnd3b

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Assertion isbnd3b M Bnd X M Met X x y X z X y M z x

Proof

Step Hyp Ref Expression
1 isbnd3 M Bnd X M Met X x M : X × X 0 x
2 metf M Met X M : X × X
3 2 adantr M Met X x M : X × X
4 ffn M : X × X M Fn X × X
5 ffnov M : X × X 0 x M Fn X × X y X z X y M z 0 x
6 5 baib M Fn X × X M : X × X 0 x y X z X y M z 0 x
7 3 4 6 3syl M Met X x M : X × X 0 x y X z X y M z 0 x
8 0red M Met X x y X z X 0
9 simplr M Met X x y X z X x
10 metcl M Met X y X z X y M z
11 10 3expb M Met X y X z X y M z
12 11 adantlr M Met X x y X z X y M z
13 metge0 M Met X y X z X 0 y M z
14 13 3expb M Met X y X z X 0 y M z
15 14 adantlr M Met X x y X z X 0 y M z
16 elicc2 0 x y M z 0 x y M z 0 y M z y M z x
17 df-3an y M z 0 y M z y M z x y M z 0 y M z y M z x
18 16 17 bitrdi 0 x y M z 0 x y M z 0 y M z y M z x
19 18 baibd 0 x y M z 0 y M z y M z 0 x y M z x
20 8 9 12 15 19 syl22anc M Met X x y X z X y M z 0 x y M z x
21 20 2ralbidva M Met X x y X z X y M z 0 x y X z X y M z x
22 7 21 bitrd M Met X x M : X × X 0 x y X z X y M z x
23 22 rexbidva M Met X x M : X × X 0 x x y X z X y M z x
24 23 pm5.32i M Met X x M : X × X 0 x M Met X x y X z X y M z x
25 1 24 bitri M Bnd X M Met X x y X z X y M z x