Step | Hyp | Ref
| Expression |
1 | | simp-4r 803 |
. . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋)) |
2 | | simplr 788 |
. . . . . 6
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+) |
3 | 2 | rphalfcld 11760 |
. . . . 5
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈
ℝ+) |
4 | | eqidd 2611 |
. . . . 5
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2)))) |
5 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2))) |
6 | 5 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝑏 = (𝑎 / 2) → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)(𝑎 / 2)))) |
7 | 6 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑏 = (𝑎 / 2) → ((◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)) ↔ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2))))) |
8 | 7 | rspcev 3282 |
. . . . 5
⊢ (((𝑎 / 2) ∈ ℝ+
∧ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) |
9 | 3, 4, 8 | syl2anc 691 |
. . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) |
10 | | metust.1 |
. . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) |
11 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏)) |
12 | 11 | imaeq2d 5385 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑏))) |
13 | 12 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑎 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) |
14 | 13 | rneqi 5273 |
. . . . . . 7
⊢ ran
(𝑎 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) |
15 | 10, 14 | eqtri 2632 |
. . . . . 6
⊢ 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) |
16 | 15 | metustel 22165 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)))) |
17 | 16 | biimpar 501 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+
(◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹) |
18 | 1, 9, 17 | syl2anc 691 |
. . 3
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹) |
19 | | relco 5550 |
. . . . 5
⊢ Rel
((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) |
20 | 19 | a1i 11 |
. . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → Rel ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
21 | | cossxp 5575 |
. . . . . . . . . 10
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) |
22 | | cnvimass 5404 |
. . . . . . . . . . . . . 14
⊢ (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷 |
23 | | psmetf 21921 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
24 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
26 | 22, 25 | syl5sseq 3616 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ (PsMet‘𝑋) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋)) |
27 | | dmss 5245 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋)) |
28 | | rnss 5275 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) |
29 | | xpss12 5148 |
. . . . . . . . . . . . . 14
⊢ ((dom
(◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) |
30 | 27, 28, 29 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) |
31 | 26, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (PsMet‘𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) |
32 | 31 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) |
33 | | dmxp 5265 |
. . . . . . . . . . . . 13
⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋) |
34 | | rnxp 5483 |
. . . . . . . . . . . . 13
⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋) |
35 | 33, 34 | xpeq12d 5064 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋)) |
36 | 35 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋)) |
37 | 32, 36 | sseqtrd 3604 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋)) |
38 | 21, 37 | syl5ss 3579 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋)) |
39 | 38 | ad3antrrr 762 |
. . . . . . . 8
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋)) |
40 | 39 | sselda 3568 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) |
41 | | opelxp 5070 |
. . . . . . 7
⊢
(〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
42 | 40, 41 | sylib 207 |
. . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
43 | | simpll 786 |
. . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
44 | | simprl 790 |
. . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑝 ∈ 𝑋) |
45 | | simprr 792 |
. . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑞 ∈ 𝑋) |
46 | | simplr 788 |
. . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
47 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
48 | 47 | simp1d 1066 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
49 | 48, 1 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋)) |
50 | 48, 2 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+) |
51 | 49, 50 | jca 553 |
. . . . . . . . . . . 12
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈
ℝ+)) |
52 | 47 | simp2d 1067 |
. . . . . . . . . . . 12
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋) |
53 | 47 | simp3d 1068 |
. . . . . . . . . . . 12
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋) |
54 | 51, 52, 53 | 3jca 1235 |
. . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
55 | | simplr 788 |
. . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋) |
56 | | simprl 790 |
. . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) |
57 | | simprr 792 |
. . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) |
58 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
59 | 58 | simp1d 1066 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈
ℝ+)) |
60 | 59 | simpld 474 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋)) |
61 | | ffun 5961 |
. . . . . . . . . . . . . 14
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun
𝐷) |
62 | 23, 61 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷) |
64 | 58 | simp2d 1067 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋) |
65 | 58 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋) |
66 | 64, 65, 41 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) |
67 | 60, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋)) |
68 | 66, 67 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑞〉 ∈ dom 𝐷) |
69 | | 0xr 9965 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈
ℝ*) |
71 | 59 | simprd 478 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+) |
72 | 71 | rpxrd 11749 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*) |
73 | 60, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
74 | 73, 66 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑞〉) ∈
ℝ*) |
75 | | psmetge0 21927 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞)) |
76 | 60, 64, 65, 75 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞)) |
77 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢ (𝑝𝐷𝑞) = (𝐷‘〈𝑝, 𝑞〉) |
78 | 76, 77 | syl6breq 4624 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘〈𝑝, 𝑞〉)) |
79 | 77, 74 | syl5eqel 2692 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈
ℝ*) |
80 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ) |
81 | 71 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ) |
82 | 81 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ) |
83 | 82 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈
ℝ*) |
84 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝𝐷𝑟) = (𝐷‘〈𝑝, 𝑟〉) |
85 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋) |
86 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑝, 𝑟〉 ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) |
87 | 64, 85, 86 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑟〉 ∈ (𝑋 × 𝑋)) |
88 | 87, 67 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑟〉 ∈ dom 𝐷) |
89 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) |
90 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) |
91 | 89, 90 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) |
92 | | fvimacnv 6240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑟〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑟〉) ∈ (0[,)(𝑎 / 2)) ↔ 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
93 | 92 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Fun
𝐷 ∧ 〈𝑝, 𝑟〉 ∈ dom 𝐷) ∧ 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘〈𝑝, 𝑟〉) ∈ (0[,)(𝑎 / 2))) |
94 | 63, 88, 91, 93 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑟〉) ∈ (0[,)(𝑎 / 2))) |
95 | 84, 94 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) |
96 | | elico2 12108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))) |
97 | 96 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))) |
98 | 97 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ) |
99 | 80, 83, 95, 98 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ) |
100 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟𝐷𝑞) = (𝐷‘〈𝑟, 𝑞〉) |
101 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑟, 𝑞〉 ∈ (𝑋 × 𝑋) ↔ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) |
102 | 85, 65, 101 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑟, 𝑞〉 ∈ (𝑋 × 𝑋)) |
103 | 102, 67 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑟, 𝑞〉 ∈ dom 𝐷) |
104 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) |
105 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) |
106 | 104, 105 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) |
107 | | fvimacnv 6240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐷 ∧ 〈𝑟, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑟, 𝑞〉) ∈ (0[,)(𝑎 / 2)) ↔ 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
108 | 107 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Fun
𝐷 ∧ 〈𝑟, 𝑞〉 ∈ dom 𝐷) ∧ 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘〈𝑟, 𝑞〉) ∈ (0[,)(𝑎 / 2))) |
109 | 63, 103, 106, 108 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑟, 𝑞〉) ∈ (0[,)(𝑎 / 2))) |
110 | 100, 109 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) |
111 | | elico2 12108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))) |
112 | 111 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))) |
113 | 112 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ) |
114 | 80, 83, 110, 113 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ) |
115 | | rexadd 11937 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑝𝐷𝑟) ∈ ℝ ∧ (𝑟𝐷𝑞) ∈ ℝ) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞))) |
116 | 99, 114, 115 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞))) |
117 | 99, 114 | readdcld 9948 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ) |
118 | 116, 117 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ) |
119 | 118 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈
ℝ*) |
120 | | psmettri 21926 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞))) |
121 | 60, 64, 65, 85, 120 | syl13anc 1320 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞))) |
122 | 97 | simp3d 1068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2)) |
123 | 80, 83, 95, 122 | syl21anc 1317 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2)) |
124 | 112 | simp3d 1068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2)) |
125 | 80, 83, 110, 124 | syl21anc 1317 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2)) |
126 | 99, 114, 81, 123, 125 | lt2halvesd 11157 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎) |
127 | 116, 126 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎) |
128 | 79, 119, 72, 121, 127 | xrlelttrd 11867 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎) |
129 | 77, 128 | syl5eqbrr 4619 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑞〉) < 𝑎) |
130 | | elico1 12089 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ*) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ ((𝐷‘〈𝑝, 𝑞〉) ∈ ℝ* ∧ 0
≤ (𝐷‘〈𝑝, 𝑞〉) ∧ (𝐷‘〈𝑝, 𝑞〉) < 𝑎))) |
131 | 130 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ (((0
∈ ℝ* ∧ 𝑎 ∈ ℝ*) ∧ ((𝐷‘〈𝑝, 𝑞〉) ∈ ℝ* ∧ 0
≤ (𝐷‘〈𝑝, 𝑞〉) ∧ (𝐷‘〈𝑝, 𝑞〉) < 𝑎)) → (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) |
132 | 70, 72, 74, 78, 129, 131 | syl23anc 1325 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) |
133 | | fvimacnv 6240 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) |
134 | 133 | biimpa 500 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) ∧ (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) → 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
135 | | df-br 4584 |
. . . . . . . . . . . . 13
⊢ (𝑝(◡𝐷 “ (0[,)𝑎))𝑞 ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) |
136 | 134, 135 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) ∧ (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞) |
137 | 63, 68, 132, 136 | syl21anc 1317 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞) |
138 | 54, 55, 56, 57, 137 | syl22anc 1319 |
. . . . . . . . . 10
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞) |
139 | 48 | simprd 478 |
. . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
140 | 139 | breqd 4594 |
. . . . . . . . . 10
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞 ↔ 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)) |
141 | 138, 140 | mpbird 246 |
. . . . . . . . 9
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞) |
142 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
143 | | df-br 4584 |
. . . . . . . . . . . . 13
⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
144 | 142, 143 | sylibr 223 |
. . . . . . . . . . . 12
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞) |
145 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑝 ∈ V |
146 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑞 ∈ V |
147 | 145, 146 | brco 5214 |
. . . . . . . . . . . 12
⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) |
148 | 144, 147 | sylib 207 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) |
149 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋)) |
150 | 149, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) |
151 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋) |
152 | 150, 151 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋) |
153 | 152 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋) |
154 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑟 ∈ V |
155 | 145, 154 | brelrn 5277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2)))) |
156 | 155 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2)))) |
157 | 153, 156 | sseldd 3569 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋) |
158 | 157 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋) |
159 | 158 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋)) |
160 | 159 | ancrd 575 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) |
161 | 160 | eximdv 1833 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) |
162 | 161 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) |
163 | 162 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) |
164 | 163 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) |
165 | 148, 164 | mpd 15 |
. . . . . . . . . 10
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))) |
166 | | df-rex 2902 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))) |
167 | 165, 166 | sylibr 223 |
. . . . . . . . 9
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) |
168 | 141, 167 | r19.29a 3060 |
. . . . . . . 8
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞) |
169 | | df-br 4584 |
. . . . . . . 8
⊢ (𝑝𝐴𝑞 ↔ 〈𝑝, 𝑞〉 ∈ 𝐴) |
170 | 168, 169 | sylib 207 |
. . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
171 | 43, 44, 45, 46, 170 | syl31anc 1321 |
. . . . . 6
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
172 | 42, 171 | mpdan 699 |
. . . . 5
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ 𝐴) |
173 | 172 | ex 449 |
. . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) → 〈𝑝, 𝑞〉 ∈ 𝐴)) |
174 | 20, 173 | relssdv 5135 |
. . 3
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) |
175 | | id 22 |
. . . . . 6
⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2)))) |
176 | 175, 175 | coeq12d 5208 |
. . . . 5
⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) |
177 | 176 | sseq1d 3595 |
. . . 4
⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)) |
178 | 177 | rspcev 3282 |
. . 3
⊢ (((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) |
179 | 18, 174, 178 | syl2anc 691 |
. 2
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) |
180 | 10 | metustel 22165 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
181 | 180 | adantl 481 |
. . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) |
182 | 181 | biimpa 500 |
. 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))) |
183 | 179, 182 | r19.29a 3060 |
1
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) |