Step | Hyp | Ref
| Expression |
1 | | isbnd 32749 |
. 2
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |
2 | | metxmet 21949 |
. . . 4
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
3 | | simpr 476 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀 ∈ (∞Met‘𝑋)) |
4 | | xmetf 21944 |
. . . . . . . 8
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ*) |
5 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑀:(𝑋 × 𝑋)⟶ℝ* → 𝑀 Fn (𝑋 × 𝑋)) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀 Fn (𝑋 × 𝑋)) |
7 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → 𝑋 = (𝑥(ball‘𝑀)𝑟)) |
8 | | rpxr 11716 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
9 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡𝑀 “ ℝ) = (◡𝑀 “ ℝ) |
10 | 9 | blssec 22050 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
11 | 10 | 3expa 1257 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
12 | 8, 11 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
13 | 12 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
14 | 7, 13 | eqsstrd 3602 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → 𝑋 ⊆ [𝑥](◡𝑀 “ ℝ)) |
15 | 14 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ [𝑥](◡𝑀 “ ℝ)) |
16 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
17 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
18 | 16, 17 | elec 7673 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ [𝑥](◡𝑀 “ ℝ) ↔ 𝑥(◡𝑀 “ ℝ)𝑦) |
19 | 15, 18 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → 𝑥(◡𝑀 “ ℝ)𝑦) |
20 | 9 | xmeterval 22047 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (∞Met‘𝑋) → (𝑥(◡𝑀 “ ℝ)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝑀𝑦) ∈ ℝ))) |
21 | 20 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → (𝑥(◡𝑀 “ ℝ)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝑀𝑦) ∈ ℝ))) |
22 | 19, 21 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝑀𝑦) ∈ ℝ)) |
23 | 22 | simp3d 1068 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑀𝑦) ∈ ℝ) |
24 | 23 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ) |
25 | 24 | rexlimdvaa 3014 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ)) |
26 | 25 | ralimdva 2945 |
. . . . . . . 8
⊢ (𝑀 ∈ (∞Met‘𝑋) → (∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ)) |
27 | 26 | impcom 445 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ) |
28 | | ffnov 6662 |
. . . . . . 7
⊢ (𝑀:(𝑋 × 𝑋)⟶ℝ ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ)) |
29 | 6, 27, 28 | sylanbrc 695 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀:(𝑋 × 𝑋)⟶ℝ) |
30 | | ismet2 21948 |
. . . . . 6
⊢ (𝑀 ∈ (Met‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ 𝑀:(𝑋 × 𝑋)⟶ℝ)) |
31 | 3, 29, 30 | sylanbrc 695 |
. . . . 5
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀 ∈ (Met‘𝑋)) |
32 | 31 | ex 449 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → (𝑀 ∈ (∞Met‘𝑋) → 𝑀 ∈ (Met‘𝑋))) |
33 | 2, 32 | impbid2 215 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → (𝑀 ∈ (Met‘𝑋) ↔ 𝑀 ∈ (∞Met‘𝑋))) |
34 | 33 | pm5.32ri 668 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |
35 | 1, 34 | bitri 263 |
1
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |