Step | Hyp | Ref
| Expression |
1 | | bndmet 35939 |
. . 3
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) |
2 | | 0re 10977 |
. . . . . 6
⊢ 0 ∈
ℝ |
3 | 2 | ne0ii 4271 |
. . . . 5
⊢ ℝ
≠ ∅ |
4 | | metf 23483 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ) |
5 | 4 | ffnd 6601 |
. . . . . . . . 9
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 Fn (𝑋 × 𝑋)) |
6 | 1, 5 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 Fn (𝑋 × 𝑋)) |
7 | 6 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀 Fn (𝑋 × 𝑋)) |
8 | 1, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ) |
9 | 8 | fdmd 6611 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (Bnd‘𝑋) → dom 𝑀 = (𝑋 × 𝑋)) |
10 | | xpeq2 5610 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = (𝑋 × ∅)) |
11 | | xp0 6061 |
. . . . . . . . . . . 12
⊢ (𝑋 × ∅) =
∅ |
12 | 10, 11 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = ∅) |
13 | 9, 12 | sylan9eq 2798 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → dom 𝑀 = ∅) |
14 | 13 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → dom 𝑀 = ∅) |
15 | | dm0rn0 5834 |
. . . . . . . . 9
⊢ (dom
𝑀 = ∅ ↔ ran
𝑀 =
∅) |
16 | 14, 15 | sylib 217 |
. . . . . . . 8
⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 = ∅) |
17 | | 0ss 4330 |
. . . . . . . 8
⊢ ∅
⊆ (0[,]𝑥) |
18 | 16, 17 | eqsstrdi 3975 |
. . . . . . 7
⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 ⊆ (0[,]𝑥)) |
19 | | df-f 6437 |
. . . . . . 7
⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ran 𝑀 ⊆ (0[,]𝑥))) |
20 | 7, 18, 19 | sylanbrc 583 |
. . . . . 6
⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
21 | 20 | ralrimiva 3103 |
. . . . 5
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
22 | | r19.2z 4425 |
. . . . 5
⊢ ((ℝ
≠ ∅ ∧ ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
23 | 3, 21, 22 | sylancr 587 |
. . . 4
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
24 | | isbnd2 35941 |
. . . . . 6
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))) |
25 | 24 | simprbi 497 |
. . . . 5
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) |
26 | | 2re 12047 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
27 | | simprlr 777 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ+) |
28 | 27 | rpred 12772 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ) |
29 | | remulcl 10956 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑟
∈ ℝ) → (2 · 𝑟) ∈ ℝ) |
30 | 26, 28, 29 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → (2 · 𝑟) ∈ ℝ) |
31 | 5 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀 Fn (𝑋 × 𝑋)) |
32 | | simpll 764 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑀 ∈ (Met‘𝑋)) |
33 | | simprl 768 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
34 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
35 | | metcl 23485 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝑀𝑧) ∈ ℝ) |
36 | 32, 33, 34, 35 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ ℝ) |
37 | | metge0 23498 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝑥𝑀𝑧)) |
38 | 32, 33, 34, 37 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑥𝑀𝑧)) |
39 | 30 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) ∈ ℝ) |
40 | | simprll 776 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑦 ∈ 𝑋) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
42 | | metcl 23485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑦𝑀𝑥) ∈ ℝ) |
43 | 32, 41, 33, 42 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) ∈ ℝ) |
44 | | metcl 23485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ) |
45 | 32, 41, 34, 44 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) ∈ ℝ) |
46 | 43, 45 | readdcld 11004 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) ∈ ℝ) |
47 | | mettri2 23494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧))) |
48 | 32, 41, 33, 34, 47 | syl13anc 1371 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧))) |
49 | 28 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ) |
50 | | simplrr 775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑋 = (𝑦(ball‘𝑀)𝑟)) |
51 | 33, 50 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ (𝑦(ball‘𝑀)𝑟)) |
52 | | metxmet 23487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
53 | 32, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑀 ∈ (∞Met‘𝑋)) |
54 | | rpxr 12739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
55 | 54 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → 𝑟 ∈ ℝ*) |
56 | 55 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ*) |
57 | | elbl2 23543 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟)) |
58 | 53, 56, 41, 33, 57 | syl22anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟)) |
59 | 51, 58 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) < 𝑟) |
60 | 34, 50 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ (𝑦(ball‘𝑀)𝑟)) |
61 | | elbl2 23543 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟)) |
62 | 53, 56, 41, 34, 61 | syl22anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟)) |
63 | 60, 62 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) < 𝑟) |
64 | 43, 45, 49, 49, 59, 63 | lt2addd 11598 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (𝑟 + 𝑟)) |
65 | 49 | recnd 11003 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℂ) |
66 | 65 | 2timesd 12216 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) = (𝑟 + 𝑟)) |
67 | 64, 66 | breqtrrd 5102 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (2 · 𝑟)) |
68 | 36, 46, 39, 48, 67 | lelttrd 11133 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) < (2 · 𝑟)) |
69 | 36, 39, 68 | ltled 11123 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ (2 · 𝑟)) |
70 | | elicc2 13144 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (2 · 𝑟) ∈ ℝ) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟)))) |
71 | 2, 39, 70 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟)))) |
72 | 36, 38, 69, 71 | mpbir3and 1341 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟))) |
73 | 72 | ralrimivva 3123 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟))) |
74 | | ffnov 7401 |
. . . . . . . . . . 11
⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))) |
75 | 31, 73, 74 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))) |
76 | | oveq2 7283 |
. . . . . . . . . . . 12
⊢ (𝑥 = (2 · 𝑟) → (0[,]𝑥) = (0[,](2 · 𝑟))) |
77 | 76 | feq3d 6587 |
. . . . . . . . . . 11
⊢ (𝑥 = (2 · 𝑟) → (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)))) |
78 | 77 | rspcev 3561 |
. . . . . . . . . 10
⊢ (((2
· 𝑟) ∈ ℝ
∧ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
79 | 30, 75, 78 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
80 | 79 | expr 457 |
. . . . . . . 8
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) |
81 | 80 | rexlimdvva 3223 |
. . . . . . 7
⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) |
82 | 1, 81 | syl 17 |
. . . . . 6
⊢ (𝑀 ∈ (Bnd‘𝑋) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) |
83 | 82 | adantr 481 |
. . . . 5
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) |
84 | 25, 83 | mpd 15 |
. . . 4
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
85 | 23, 84 | pm2.61dane 3032 |
. . 3
⊢ (𝑀 ∈ (Bnd‘𝑋) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
86 | 1, 85 | jca 512 |
. 2
⊢ (𝑀 ∈ (Bnd‘𝑋) → (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) |
87 | | simpll 764 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Met‘𝑋)) |
88 | | simpllr 773 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ ℝ) |
89 | 87 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀 ∈ (Met‘𝑋)) |
90 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
91 | | met0 23496 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) = 0) |
92 | 89, 90, 91 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) = 0) |
93 | | simplr 766 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) |
94 | 93, 90, 90 | fovrnd 7444 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ∈ (0[,]𝑥)) |
95 | | elicc2 13144 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝑥
∈ ℝ) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥))) |
96 | 2, 88, 95 | sylancr 587 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥))) |
97 | 94, 96 | mpbid 231 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)) |
98 | 97 | simp3d 1143 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ≤ 𝑥) |
99 | 92, 98 | eqbrtrrd 5098 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 0 ≤ 𝑥) |
100 | 88, 99 | ge0p1rpd 12802 |
. . . . . 6
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈
ℝ+) |
101 | | fovrn 7442 |
. . . . . . . . . . . . . 14
⊢ ((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥)) |
102 | 101 | 3expa 1117 |
. . . . . . . . . . . . 13
⊢ (((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥)) |
103 | 102 | adantlll 715 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥)) |
104 | | elicc2 13144 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 𝑥
∈ ℝ) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥))) |
105 | 2, 88, 104 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥))) |
106 | 105 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥))) |
107 | 103, 106 | mpbid 231 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)) |
108 | 107 | simp1d 1141 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ) |
109 | 88 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 ∈ ℝ) |
110 | | peano2re 11148 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
111 | 88, 110 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ) |
112 | 111 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ) |
113 | 107 | simp3d 1143 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ≤ 𝑥) |
114 | 109 | ltp1d 11905 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 < (𝑥 + 1)) |
115 | 108, 109,
112, 113, 114 | lelttrd 11133 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
(Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) < (𝑥 + 1)) |
116 | 115 | ralrimiva 3103 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) < (𝑥 + 1)) |
117 | | rabid2 3314 |
. . . . . . . 8
⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)} ↔ ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) < (𝑥 + 1)) |
118 | 116, 117 | sylibr 233 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)}) |
119 | 89, 52 | syl 17 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
120 | 111 | rexrd 11025 |
. . . . . . . 8
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈
ℝ*) |
121 | | blval 23539 |
. . . . . . . 8
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑥 + 1) ∈ ℝ*) →
(𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)}) |
122 | 119, 90, 120, 121 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)}) |
123 | 118, 122 | eqtr4d 2781 |
. . . . . 6
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))) |
124 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑟 = (𝑥 + 1) → (𝑦(ball‘𝑀)𝑟) = (𝑦(ball‘𝑀)(𝑥 + 1))) |
125 | 124 | rspceeqv 3575 |
. . . . . 6
⊢ (((𝑥 + 1) ∈ ℝ+
∧ 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) |
126 | 100, 123,
125 | syl2anc 584 |
. . . . 5
⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) |
127 | 126 | ralrimiva 3103 |
. . . 4
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)) |
128 | | isbnd 35938 |
. . . 4
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))) |
129 | 87, 127, 128 | sylanbrc 583 |
. . 3
⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋)) |
130 | 129 | r19.29an 3217 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋)) |
131 | 86, 130 | impbii 208 |
1
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) |