Step | Hyp | Ref
| Expression |
1 | | isbnd 37188 |
. 2
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |
2 | | metxmet 24227 |
. . . 4
⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋)) |
3 | | simpr 484 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀 ∈ (∞Met‘𝑋)) |
4 | | xmetf 24222 |
. . . . . . . 8
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ*) |
5 | | ffn 6716 |
. . . . . . . 8
⊢ (𝑀:(𝑋 × 𝑋)⟶ℝ* → 𝑀 Fn (𝑋 × 𝑋)) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀 Fn (𝑋 × 𝑋)) |
7 | | simprr 772 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → 𝑋 = (𝑥(ball‘𝑀)𝑟)) |
8 | | rpxr 13007 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
9 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡𝑀 “ ℝ) = (◡𝑀 “ ℝ) |
10 | 9 | blssec 24328 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
11 | 10 | 3expa 1116 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
12 | 8, 11 | sylan2 592 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
13 | 12 | adantrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → (𝑥(ball‘𝑀)𝑟) ⊆ [𝑥](◡𝑀 “ ℝ)) |
14 | 7, 13 | eqsstrd 4016 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → 𝑋 ⊆ [𝑥](◡𝑀 “ ℝ)) |
15 | 14 | sselda 3978 |
. . . . . . . . . . . . . 14
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ [𝑥](◡𝑀 “ ℝ)) |
16 | | vex 3473 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
17 | | vex 3473 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
18 | 16, 17 | elec 8763 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ [𝑥](◡𝑀 “ ℝ) ↔ 𝑥(◡𝑀 “ ℝ)𝑦) |
19 | 15, 18 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → 𝑥(◡𝑀 “ ℝ)𝑦) |
20 | 9 | xmeterval 24325 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (∞Met‘𝑋) → (𝑥(◡𝑀 “ ℝ)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝑀𝑦) ∈ ℝ))) |
21 | 20 | ad3antrrr 729 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → (𝑥(◡𝑀 “ ℝ)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝑀𝑦) ∈ ℝ))) |
22 | 19, 21 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝑀𝑦) ∈ ℝ)) |
23 | 22 | simp3d 1142 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑀𝑦) ∈ ℝ) |
24 | 23 | ralrimiva 3141 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑋 = (𝑥(ball‘𝑀)𝑟))) → ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ) |
25 | 24 | rexlimdvaa 3151 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ)) |
26 | 25 | ralimdva 3162 |
. . . . . . . 8
⊢ (𝑀 ∈ (∞Met‘𝑋) → (∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ)) |
27 | 26 | impcom 407 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ) |
28 | | ffnov 7541 |
. . . . . . 7
⊢ (𝑀:(𝑋 × 𝑋)⟶ℝ ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) ∈ ℝ)) |
29 | 6, 27, 28 | sylanbrc 582 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀:(𝑋 × 𝑋)⟶ℝ) |
30 | | ismet2 24226 |
. . . . . 6
⊢ (𝑀 ∈ (Met‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ 𝑀:(𝑋 × 𝑋)⟶ℝ)) |
31 | 3, 29, 30 | sylanbrc 582 |
. . . . 5
⊢
((∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) ∧ 𝑀 ∈ (∞Met‘𝑋)) → 𝑀 ∈ (Met‘𝑋)) |
32 | 31 | ex 412 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → (𝑀 ∈ (∞Met‘𝑋) → 𝑀 ∈ (Met‘𝑋))) |
33 | 2, 32 | impbid2 225 |
. . 3
⊢
(∀𝑥 ∈
𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟) → (𝑀 ∈ (Met‘𝑋) ↔ 𝑀 ∈ (∞Met‘𝑋))) |
34 | 33 | pm5.32ri 575 |
. 2
⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |
35 | 1, 34 | bitri 275 |
1
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) |