| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝐷 ∈ (∞Met‘𝑋)) |
| 2 | | xmetresbl.1 |
. . . 4
⊢ 𝐵 = (𝑃(ball‘𝐷)𝑅) |
| 3 | | blssm 24428 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋) |
| 4 | 2, 3 | eqsstrid 4022 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝐵 ⊆ 𝑋) |
| 5 | | xmetres2 24371 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ⊆ 𝑋) → (𝐷 ↾ (𝐵 × 𝐵)) ∈ (∞Met‘𝐵)) |
| 6 | 1, 4, 5 | syl2anc 584 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)) ∈ (∞Met‘𝐵)) |
| 7 | | xmetf 24339 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 8 | 1, 7 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 9 | | xpss12 5700 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → (𝐵 × 𝐵) ⊆ (𝑋 × 𝑋)) |
| 10 | 4, 4, 9 | syl2anc 584 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐵 × 𝐵) ⊆ (𝑋 × 𝑋)) |
| 11 | 8, 10 | fssresd 6775 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶ℝ*) |
| 12 | 11 | ffnd 6737 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵)) |
| 13 | | ovres 7599 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(𝐷 ↾ (𝐵 × 𝐵))𝑦) = (𝑥𝐷𝑦)) |
| 14 | 13 | adantl 481 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝐷 ↾ (𝐵 × 𝐵))𝑦) = (𝑥𝐷𝑦)) |
| 15 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 16 | | eqid 2737 |
. . . . . . . . . 10
⊢ (◡𝐷 “ ℝ) = (◡𝐷 “ ℝ) |
| 17 | 16 | xmeter 24443 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → (◡𝐷 “ ℝ) Er 𝑋) |
| 18 | 15, 17 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (◡𝐷 “ ℝ) Er 𝑋) |
| 19 | 16 | blssec 24445 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ [𝑃](◡𝐷 “ ℝ)) |
| 20 | 2, 19 | eqsstrid 4022 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝐵 ⊆ [𝑃](◡𝐷 “ ℝ)) |
| 21 | 20 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ [𝑃](◡𝐷 “ ℝ)) |
| 22 | 21 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ [𝑃](◡𝐷 “ ℝ)) |
| 23 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ 𝑋) |
| 24 | | elecg 8789 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ [𝑃](◡𝐷 “ ℝ) ∧ 𝑃 ∈ 𝑋) → (𝑥 ∈ [𝑃](◡𝐷 “ ℝ) ↔ 𝑃(◡𝐷 “ ℝ)𝑥)) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ∈ [𝑃](◡𝐷 “ ℝ) ↔ 𝑃(◡𝐷 “ ℝ)𝑥)) |
| 26 | 22, 25 | mpbid 232 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃(◡𝐷 “ ℝ)𝑥) |
| 27 | 20 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ [𝑃](◡𝐷 “ ℝ)) |
| 28 | 27 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ [𝑃](◡𝐷 “ ℝ)) |
| 29 | | elecg 8789 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ [𝑃](◡𝐷 “ ℝ) ∧ 𝑃 ∈ 𝑋) → (𝑦 ∈ [𝑃](◡𝐷 “ ℝ) ↔ 𝑃(◡𝐷 “ ℝ)𝑦)) |
| 30 | 28, 23, 29 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ [𝑃](◡𝐷 “ ℝ) ↔ 𝑃(◡𝐷 “ ℝ)𝑦)) |
| 31 | 28, 30 | mpbid 232 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃(◡𝐷 “ ℝ)𝑦) |
| 32 | 18, 26, 31 | ertr3d 8763 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥(◡𝐷 “ ℝ)𝑦) |
| 33 | 16 | xmeterval 24442 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥(◡𝐷 “ ℝ)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ))) |
| 34 | 15, 33 | syl 17 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(◡𝐷 “ ℝ)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ))) |
| 35 | 32, 34 | mpbid 232 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ)) |
| 36 | 35 | simp3d 1145 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐷𝑦) ∈ ℝ) |
| 37 | 14, 36 | eqeltrd 2841 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝐷 ↾ (𝐵 × 𝐵))𝑦) ∈ ℝ) |
| 38 | 37 | ralrimivva 3202 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(𝐷 ↾ (𝐵 × 𝐵))𝑦) ∈ ℝ) |
| 39 | | ffnov 7559 |
. . 3
⊢ ((𝐷 ↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶ℝ ↔ ((𝐷 ↾ (𝐵 × 𝐵)) Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(𝐷 ↾ (𝐵 × 𝐵))𝑦) ∈ ℝ)) |
| 40 | 12, 38, 39 | sylanbrc 583 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶ℝ) |
| 41 | | ismet2 24343 |
. 2
⊢ ((𝐷 ↾ (𝐵 × 𝐵)) ∈ (Met‘𝐵) ↔ ((𝐷 ↾ (𝐵 × 𝐵)) ∈ (∞Met‘𝐵) ∧ (𝐷 ↾ (𝐵 × 𝐵)):(𝐵 × 𝐵)⟶ℝ)) |
| 42 | 6, 40, 41 | sylanbrc 583 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)) ∈ (Met‘𝐵)) |