Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isbnd3 Structured version   Visualization version   GIF version

Theorem isbnd3 33201
Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.)
Assertion
Ref Expression
isbnd3 (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
Distinct variable groups:   𝑥,𝑀   𝑥,𝑋

Proof of Theorem isbnd3
Dummy variables 𝑟 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bndmet 33198 . . 3 (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
2 0re 9985 . . . . . 6 0 ∈ ℝ
32ne0ii 3904 . . . . 5 ℝ ≠ ∅
4 metf 22040 . . . . . . . . . 10 (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
5 ffn 6004 . . . . . . . . . 10 (𝑀:(𝑋 × 𝑋)⟶ℝ → 𝑀 Fn (𝑋 × 𝑋))
64, 5syl 17 . . . . . . . . 9 (𝑀 ∈ (Met‘𝑋) → 𝑀 Fn (𝑋 × 𝑋))
71, 6syl 17 . . . . . . . 8 (𝑀 ∈ (Bnd‘𝑋) → 𝑀 Fn (𝑋 × 𝑋))
87ad2antrr 761 . . . . . . 7 (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀 Fn (𝑋 × 𝑋))
91, 4syl 17 . . . . . . . . . . . 12 (𝑀 ∈ (Bnd‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
10 fdm 6010 . . . . . . . . . . . 12 (𝑀:(𝑋 × 𝑋)⟶ℝ → dom 𝑀 = (𝑋 × 𝑋))
119, 10syl 17 . . . . . . . . . . 11 (𝑀 ∈ (Bnd‘𝑋) → dom 𝑀 = (𝑋 × 𝑋))
12 xpeq2 5094 . . . . . . . . . . . 12 (𝑋 = ∅ → (𝑋 × 𝑋) = (𝑋 × ∅))
13 xp0 5515 . . . . . . . . . . . 12 (𝑋 × ∅) = ∅
1412, 13syl6eq 2676 . . . . . . . . . . 11 (𝑋 = ∅ → (𝑋 × 𝑋) = ∅)
1511, 14sylan9eq 2680 . . . . . . . . . 10 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → dom 𝑀 = ∅)
1615adantr 481 . . . . . . . . 9 (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → dom 𝑀 = ∅)
17 dm0rn0 5306 . . . . . . . . 9 (dom 𝑀 = ∅ ↔ ran 𝑀 = ∅)
1816, 17sylib 208 . . . . . . . 8 (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 = ∅)
19 0ss 3949 . . . . . . . 8 ∅ ⊆ (0[,]𝑥)
2018, 19syl6eqss 3639 . . . . . . 7 (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 ⊆ (0[,]𝑥))
21 df-f 5854 . . . . . . 7 (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ran 𝑀 ⊆ (0[,]𝑥)))
228, 20, 21sylanbrc 697 . . . . . 6 (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
2322ralrimiva 2965 . . . . 5 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
24 r19.2z 4037 . . . . 5 ((ℝ ≠ ∅ ∧ ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
253, 23, 24sylancr 694 . . . 4 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
26 isbnd2 33200 . . . . . 6 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
2726simprbi 480 . . . . 5 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
28 2re 11035 . . . . . . . . . . 11 2 ∈ ℝ
29 simprlr 802 . . . . . . . . . . . 12 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ+)
3029rpred 11816 . . . . . . . . . . 11 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ)
31 remulcl 9966 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (2 · 𝑟) ∈ ℝ)
3228, 30, 31sylancr 694 . . . . . . . . . 10 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → (2 · 𝑟) ∈ ℝ)
336adantr 481 . . . . . . . . . . 11 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀 Fn (𝑋 × 𝑋))
34 simpll 789 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑀 ∈ (Met‘𝑋))
35 simprl 793 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑥𝑋)
36 simprr 795 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑧𝑋)
37 metcl 22042 . . . . . . . . . . . . . 14 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥𝑋𝑧𝑋) → (𝑥𝑀𝑧) ∈ ℝ)
3834, 35, 36, 37syl3anc 1323 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑥𝑀𝑧) ∈ ℝ)
39 metge0 22055 . . . . . . . . . . . . . 14 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥𝑋𝑧𝑋) → 0 ≤ (𝑥𝑀𝑧))
4034, 35, 36, 39syl3anc 1323 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 0 ≤ (𝑥𝑀𝑧))
4132adantr 481 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (2 · 𝑟) ∈ ℝ)
42 simprll 801 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑦𝑋)
4342adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑦𝑋)
44 metcl 22042 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦𝑋𝑥𝑋) → (𝑦𝑀𝑥) ∈ ℝ)
4534, 43, 35, 44syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑦𝑀𝑥) ∈ ℝ)
46 metcl 22042 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦𝑋𝑧𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
4734, 43, 36, 46syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑦𝑀𝑧) ∈ ℝ)
4845, 47readdcld 10014 . . . . . . . . . . . . . . 15 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) ∈ ℝ)
49 mettri2 22051 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦𝑋𝑥𝑋𝑧𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)))
5034, 43, 35, 36, 49syl13anc 1325 . . . . . . . . . . . . . . 15 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)))
5130adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑟 ∈ ℝ)
52 simplrr 800 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑋 = (𝑦(ball‘𝑀)𝑟))
5335, 52eleqtrd 2706 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑥 ∈ (𝑦(ball‘𝑀)𝑟))
54 metxmet 22044 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
5534, 54syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑀 ∈ (∞Met‘𝑋))
56 rpxr 11784 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
5756ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → 𝑟 ∈ ℝ*)
5857ad2antlr 762 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑟 ∈ ℝ*)
59 elbl2 22100 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦𝑋𝑥𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟))
6055, 58, 43, 35, 59syl22anc 1324 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟))
6153, 60mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑦𝑀𝑥) < 𝑟)
6236, 52eleqtrd 2706 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑧 ∈ (𝑦(ball‘𝑀)𝑟))
63 elbl2 22100 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦𝑋𝑧𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟))
6455, 58, 43, 36, 63syl22anc 1324 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟))
6562, 64mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑦𝑀𝑧) < 𝑟)
6645, 47, 51, 51, 61, 65lt2addd 10595 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (𝑟 + 𝑟))
6751recnd 10013 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → 𝑟 ∈ ℂ)
68672timesd 11220 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (2 · 𝑟) = (𝑟 + 𝑟))
6966, 68breqtrrd 4646 . . . . . . . . . . . . . . 15 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (2 · 𝑟))
7038, 48, 41, 50, 69lelttrd 10140 . . . . . . . . . . . . . 14 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑥𝑀𝑧) < (2 · 𝑟))
7138, 41, 70ltled 10130 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑥𝑀𝑧) ≤ (2 · 𝑟))
72 elicc2 12177 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (2 · 𝑟) ∈ ℝ) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟))))
732, 41, 72sylancr 694 . . . . . . . . . . . . 13 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟))))
7438, 40, 71, 73mpbir3and 1243 . . . . . . . . . . . 12 (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥𝑋𝑧𝑋)) → (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
7574ralrimivva 2970 . . . . . . . . . . 11 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∀𝑥𝑋𝑧𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
76 ffnov 6718 . . . . . . . . . . 11 (𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥𝑋𝑧𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟))))
7733, 75, 76sylanbrc 697 . . . . . . . . . 10 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)))
78 oveq2 6613 . . . . . . . . . . . 12 (𝑥 = (2 · 𝑟) → (0[,]𝑥) = (0[,](2 · 𝑟)))
7978feq3d 5991 . . . . . . . . . . 11 (𝑥 = (2 · 𝑟) → (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))))
8079rspcev 3300 . . . . . . . . . 10 (((2 · 𝑟) ∈ ℝ ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
8132, 77, 80syl2anc 692 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦𝑋𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
8281expr 642 . . . . . . . 8 ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦𝑋𝑟 ∈ ℝ+)) → (𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
8382rexlimdvva 3036 . . . . . . 7 (𝑀 ∈ (Met‘𝑋) → (∃𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
841, 83syl 17 . . . . . 6 (𝑀 ∈ (Bnd‘𝑋) → (∃𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
8584adantr 481 . . . . 5 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → (∃𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
8627, 85mpd 15 . . . 4 ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
8725, 86pm2.61dane 2883 . . 3 (𝑀 ∈ (Bnd‘𝑋) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
881, 87jca 554 . 2 (𝑀 ∈ (Bnd‘𝑋) → (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
89 simpll 789 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Met‘𝑋))
90 simpllr 798 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑥 ∈ ℝ)
9189adantr 481 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑀 ∈ (Met‘𝑋))
92 simpr 477 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑦𝑋)
93 met0 22053 . . . . . . . . 9 ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦𝑋) → (𝑦𝑀𝑦) = 0)
9491, 92, 93syl2anc 692 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑦𝑀𝑦) = 0)
95 simplr 791 . . . . . . . . . . 11 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
9695, 92, 92fovrnd 6760 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑦𝑀𝑦) ∈ (0[,]𝑥))
97 elicc2 12177 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)))
982, 90, 97sylancr 694 . . . . . . . . . 10 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)))
9996, 98mpbid 222 . . . . . . . . 9 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥))
10099simp3d 1073 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑦𝑀𝑦) ≤ 𝑥)
10194, 100eqbrtrrd 4642 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 0 ≤ 𝑥)
10290, 101ge0p1rpd 11846 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑥 + 1) ∈ ℝ+)
103 fovrn 6758 . . . . . . . . . . . . . 14 ((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦𝑋𝑧𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
1041033expa 1262 . . . . . . . . . . . . 13 (((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
105104adantlll 753 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
106 elicc2 12177 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
1072, 90, 106sylancr 694 . . . . . . . . . . . . 13 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
108107adantr 481 . . . . . . . . . . . 12 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
109105, 108mpbid 222 . . . . . . . . . . 11 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥))
110109simp1d 1071 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
11190adantr 481 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → 𝑥 ∈ ℝ)
112 peano2re 10154 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
11390, 112syl 17 . . . . . . . . . . 11 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑥 + 1) ∈ ℝ)
114113adantr 481 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → (𝑥 + 1) ∈ ℝ)
115109simp3d 1073 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → (𝑦𝑀𝑧) ≤ 𝑥)
116111ltp1d 10899 . . . . . . . . . 10 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → 𝑥 < (𝑥 + 1))
117110, 111, 114, 115, 116lelttrd 10140 . . . . . . . . 9 (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) ∧ 𝑧𝑋) → (𝑦𝑀𝑧) < (𝑥 + 1))
118117ralrimiva 2965 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → ∀𝑧𝑋 (𝑦𝑀𝑧) < (𝑥 + 1))
119 rabid2 3112 . . . . . . . 8 (𝑋 = {𝑧𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)} ↔ ∀𝑧𝑋 (𝑦𝑀𝑧) < (𝑥 + 1))
120118, 119sylibr 224 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑋 = {𝑧𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
12191, 54syl 17 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑀 ∈ (∞Met‘𝑋))
122113rexrd 10034 . . . . . . . 8 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑥 + 1) ∈ ℝ*)
123 blval 22096 . . . . . . . 8 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑥 + 1) ∈ ℝ*) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
124121, 92, 122, 123syl3anc 1323 . . . . . . 7 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
125120, 124eqtr4d 2663 . . . . . 6 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1)))
126 oveq2 6613 . . . . . . . 8 (𝑟 = (𝑥 + 1) → (𝑦(ball‘𝑀)𝑟) = (𝑦(ball‘𝑀)(𝑥 + 1)))
127126eqeq2d 2636 . . . . . . 7 (𝑟 = (𝑥 + 1) → (𝑋 = (𝑦(ball‘𝑀)𝑟) ↔ 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))))
128127rspcev 3300 . . . . . 6 (((𝑥 + 1) ∈ ℝ+𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
129102, 125, 128syl2anc 692 . . . . 5 ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦𝑋) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
130129ralrimiva 2965 . . . 4 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∀𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
131 isbnd 33197 . . . 4 (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦𝑋𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
13289, 130, 131sylanbrc 697 . . 3 (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
133132r19.29an 3075 . 2 ((𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
13488, 133impbii 199 1 (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1992  wne 2796  wral 2912  wrex 2913  {crab 2916  wss 3560  c0 3896   class class class wbr 4618   × cxp 5077  dom cdm 5079  ran crn 5080   Fn wfn 5845  wf 5846  cfv 5850  (class class class)co 6605  cr 9880  0cc0 9881  1c1 9882   + caddc 9884   · cmul 9886  *cxr 10018   < clt 10019  cle 10020  2c2 11015  +crp 11776  [,]cicc 12117  ∞Metcxmt 19645  Metcme 19646  ballcbl 19647  Bndcbnd 33184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-1st 7116  df-2nd 7117  df-er 7688  df-ec 7690  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-2 11024  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-icc 12121  df-psmet 19652  df-xmet 19653  df-met 19654  df-bl 19655  df-bnd 33196
This theorem is referenced by:  isbnd3b  33202  prdsbnd  33210
  Copyright terms: Public domain W3C validator