| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp-4r 783 | . . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋)) | 
| 2 |  | simplr 768 | . . . . . 6
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+) | 
| 3 | 2 | rphalfcld 13090 | . . . . 5
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈
ℝ+) | 
| 4 |  | eqidd 2737 | . . . . 5
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 5 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2))) | 
| 6 | 5 | imaeq2d 6077 | . . . . . 6
⊢ (𝑏 = (𝑎 / 2) → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 7 | 6 | rspceeqv 3644 | . . . . 5
⊢ (((𝑎 / 2) ∈ ℝ+
∧ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) | 
| 8 | 3, 4, 7 | syl2anc 584 | . . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) | 
| 9 |  | metust.1 | . . . . . . 7
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) | 
| 10 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏)) | 
| 11 | 10 | imaeq2d 6077 | . . . . . . . . 9
⊢ (𝑎 = 𝑏 → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑏))) | 
| 12 | 11 | cbvmptv 5254 | . . . . . . . 8
⊢ (𝑎 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) | 
| 13 | 12 | rneqi 5947 | . . . . . . 7
⊢ ran
(𝑎 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) | 
| 14 | 9, 13 | eqtri 2764 | . . . . . 6
⊢ 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏))) | 
| 15 | 14 | metustel 24564 | . . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)))) | 
| 16 | 15 | biimpar 477 | . . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+
(◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹) | 
| 17 | 1, 8, 16 | syl2anc 584 | . . 3
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹) | 
| 18 |  | relco 6125 | . . . . 5
⊢ Rel
((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 19 | 18 | a1i 11 | . . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → Rel ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 20 |  | cossxp 6291 | . . . . . . . . . 10
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 21 |  | cnvimass 6099 | . . . . . . . . . . . . . 14
⊢ (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷 | 
| 22 |  | psmetf 24317 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | 
| 23 | 21, 22 | fssdm 6754 | . . . . . . . . . . . . 13
⊢ (𝐷 ∈ (PsMet‘𝑋) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋)) | 
| 24 |  | dmss 5912 | . . . . . . . . . . . . . 14
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋)) | 
| 25 |  | rnss 5949 | . . . . . . . . . . . . . 14
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) | 
| 26 |  | xpss12 5699 | . . . . . . . . . . . . . 14
⊢ ((dom
(◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) | 
| 27 | 24, 25, 26 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) | 
| 28 | 23, 27 | syl 17 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ (PsMet‘𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) | 
| 29 | 28 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋))) | 
| 30 |  | dmxp 5938 | . . . . . . . . . . . . 13
⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋) | 
| 31 |  | rnxp 6189 | . . . . . . . . . . . . 13
⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋) | 
| 32 | 30, 31 | xpeq12d 5715 | . . . . . . . . . . . 12
⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋)) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋)) | 
| 34 | 29, 33 | sseqtrd 4019 | . . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋)) | 
| 35 | 20, 34 | sstrid 3994 | . . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋)) | 
| 36 | 35 | ad3antrrr 730 | . . . . . . . 8
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋)) | 
| 37 | 36 | sselda 3982 | . . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) | 
| 38 |  | opelxp 5720 | . . . . . . 7
⊢
(〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) | 
| 39 | 37, 38 | sylib 218 | . . . . . 6
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) | 
| 40 |  | simpll 766 | . . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) | 
| 41 |  | simprl 770 | . . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑝 ∈ 𝑋) | 
| 42 |  | simprr 772 | . . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑞 ∈ 𝑋) | 
| 43 |  | simplr 768 | . . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 44 |  | simplll 774 | . . . . . . . . . . . . . . 15
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) | 
| 45 | 44 | simp1d 1142 | . . . . . . . . . . . . . 14
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) | 
| 46 | 45, 1 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋)) | 
| 47 | 45, 2 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+) | 
| 48 | 46, 47 | jca 511 | . . . . . . . . . . . 12
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈
ℝ+)) | 
| 49 | 44 | simp2d 1143 | . . . . . . . . . . . 12
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋) | 
| 50 | 44 | simp3d 1144 | . . . . . . . . . . . 12
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋) | 
| 51 | 48, 49, 50 | 3jca 1128 | . . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) | 
| 52 |  | simplr 768 | . . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋) | 
| 53 |  | simprl 770 | . . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) | 
| 54 |  | simprr 772 | . . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) | 
| 55 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) | 
| 56 | 55 | simp1d 1142 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈
ℝ+)) | 
| 57 | 56 | simpld 494 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋)) | 
| 58 | 22 | ffund 6739 | . . . . . . . . . . . . 13
⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷) | 
| 60 | 55 | simp2d 1143 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋) | 
| 61 | 55 | simp3d 1144 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋) | 
| 62 | 60, 61 | opelxpd 5723 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑞〉 ∈ (𝑋 × 𝑋)) | 
| 63 | 22 | fdmd 6745 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) | 
| 64 | 57, 63 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋)) | 
| 65 | 62, 64 | eleqtrrd 2843 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑞〉 ∈ dom 𝐷) | 
| 66 |  | 0xr 11309 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* | 
| 67 | 66 | a1i 11 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈
ℝ*) | 
| 68 | 56 | simprd 495 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+) | 
| 69 | 68 | rpxrd 13079 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*) | 
| 70 | 57, 22 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | 
| 71 | 70, 62 | ffvelcdmd 7104 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑞〉) ∈
ℝ*) | 
| 72 |  | psmetge0 24323 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞)) | 
| 73 | 57, 60, 61, 72 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞)) | 
| 74 |  | df-ov 7435 | . . . . . . . . . . . . . 14
⊢ (𝑝𝐷𝑞) = (𝐷‘〈𝑝, 𝑞〉) | 
| 75 | 73, 74 | breqtrdi 5183 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘〈𝑝, 𝑞〉)) | 
| 76 | 74, 71 | eqeltrid 2844 | . . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈
ℝ*) | 
| 77 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ) | 
| 78 | 68 | rpred 13078 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ) | 
| 79 | 78 | rehalfcld 12515 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ) | 
| 80 | 79 | rexrd 11312 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈
ℝ*) | 
| 81 |  | df-ov 7435 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝𝐷𝑟) = (𝐷‘〈𝑝, 𝑟〉) | 
| 82 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋) | 
| 83 | 60, 82 | opelxpd 5723 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑟〉 ∈ (𝑋 × 𝑋)) | 
| 84 | 83, 64 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑟〉 ∈ dom 𝐷) | 
| 85 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) | 
| 86 |  | df-br 5143 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 87 | 85, 86 | sylib 218 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 88 |  | fvimacnv 7072 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑟〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑟〉) ∈ (0[,)(𝑎 / 2)) ↔ 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 89 | 88 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((Fun
𝐷 ∧ 〈𝑝, 𝑟〉 ∈ dom 𝐷) ∧ 〈𝑝, 𝑟〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘〈𝑝, 𝑟〉) ∈ (0[,)(𝑎 / 2))) | 
| 90 | 59, 84, 87, 89 | syl21anc 837 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑟〉) ∈ (0[,)(𝑎 / 2))) | 
| 91 | 81, 90 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) | 
| 92 |  | elico2 13452 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))) | 
| 93 | 92 | biimpa 476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))) | 
| 94 | 93 | simp1d 1142 | . . . . . . . . . . . . . . . . . . 19
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ) | 
| 95 | 77, 80, 91, 94 | syl21anc 837 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ) | 
| 96 |  | df-ov 7435 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟𝐷𝑞) = (𝐷‘〈𝑟, 𝑞〉) | 
| 97 | 82, 61 | opelxpd 5723 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑟, 𝑞〉 ∈ (𝑋 × 𝑋)) | 
| 98 | 97, 64 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑟, 𝑞〉 ∈ dom 𝐷) | 
| 99 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) | 
| 100 |  | df-br 5143 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 101 | 99, 100 | sylib 218 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 102 |  | fvimacnv 7072 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐷 ∧ 〈𝑟, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑟, 𝑞〉) ∈ (0[,)(𝑎 / 2)) ↔ 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 103 | 102 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((Fun
𝐷 ∧ 〈𝑟, 𝑞〉 ∈ dom 𝐷) ∧ 〈𝑟, 𝑞〉 ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘〈𝑟, 𝑞〉) ∈ (0[,)(𝑎 / 2))) | 
| 104 | 59, 98, 101, 103 | syl21anc 837 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑟, 𝑞〉) ∈ (0[,)(𝑎 / 2))) | 
| 105 | 96, 104 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) | 
| 106 |  | elico2 13452 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))) | 
| 107 | 106 | biimpa 476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))) | 
| 108 | 107 | simp1d 1142 | . . . . . . . . . . . . . . . . . . 19
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ) | 
| 109 | 77, 80, 105, 108 | syl21anc 837 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ) | 
| 110 | 95, 109 | rexaddd 13277 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞))) | 
| 111 | 95, 109 | readdcld 11291 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ) | 
| 112 | 110, 111 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ) | 
| 113 | 112 | rexrd 11312 | . . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈
ℝ*) | 
| 114 |  | psmettri 24322 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞))) | 
| 115 | 57, 60, 61, 82, 114 | syl13anc 1373 | . . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞))) | 
| 116 | 93 | simp3d 1144 | . . . . . . . . . . . . . . . . . 18
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2)) | 
| 117 | 77, 80, 91, 116 | syl21anc 837 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2)) | 
| 118 | 107 | simp3d 1144 | . . . . . . . . . . . . . . . . . 18
⊢ (((0
∈ ℝ ∧ (𝑎 /
2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2)) | 
| 119 | 77, 80, 105, 118 | syl21anc 837 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2)) | 
| 120 | 95, 109, 78, 117, 119 | lt2halvesd 12516 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎) | 
| 121 | 110, 120 | eqbrtrd 5164 | . . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎) | 
| 122 | 76, 113, 69, 115, 121 | xrlelttrd 13203 | . . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎) | 
| 123 | 74, 122 | eqbrtrrid 5178 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑞〉) < 𝑎) | 
| 124 | 67, 69, 71, 75, 123 | elicod 13438 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) | 
| 125 |  | fvimacnv 7072 | . . . . . . . . . . . . . 14
⊢ ((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) → ((𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎) ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎)))) | 
| 126 | 125 | biimpa 476 | . . . . . . . . . . . . 13
⊢ (((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) ∧ (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) → 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) | 
| 127 |  | df-br 5143 | . . . . . . . . . . . . 13
⊢ (𝑝(◡𝐷 “ (0[,)𝑎))𝑞 ↔ 〈𝑝, 𝑞〉 ∈ (◡𝐷 “ (0[,)𝑎))) | 
| 128 | 126, 127 | sylibr 234 | . . . . . . . . . . . 12
⊢ (((Fun
𝐷 ∧ 〈𝑝, 𝑞〉 ∈ dom 𝐷) ∧ (𝐷‘〈𝑝, 𝑞〉) ∈ (0[,)𝑎)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞) | 
| 129 | 59, 65, 124, 128 | syl21anc 837 | . . . . . . . . . . 11
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+)
∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞) | 
| 130 | 51, 52, 53, 54, 129 | syl22anc 838 | . . . . . . . . . 10
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞) | 
| 131 | 45 | simprd 495 | . . . . . . . . . . 11
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (◡𝐷 “ (0[,)𝑎))) | 
| 132 | 131 | breqd 5153 | . . . . . . . . . 10
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞 ↔ 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)) | 
| 133 | 130, 132 | mpbird 257 | . . . . . . . . 9
⊢
(((((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞) | 
| 134 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 135 |  | df-br 5143 | . . . . . . . . . . . . 13
⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 136 | 134, 135 | sylibr 234 | . . . . . . . . . . . 12
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞) | 
| 137 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑝 ∈ V | 
| 138 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑞 ∈ V | 
| 139 | 137, 138 | brco 5880 | . . . . . . . . . . . 12
⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) | 
| 140 | 136, 139 | sylib 218 | . . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) | 
| 141 | 23 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋)) | 
| 142 | 141, 25 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) | 
| 143 | 31 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋) | 
| 144 | 142, 143 | sseqtrd 4019 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋) | 
| 145 | 144 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋) | 
| 146 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑟 ∈ V | 
| 147 | 137, 146 | brelrn 5952 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 148 | 147 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 149 | 145, 148 | sseldd 3983 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋) | 
| 150 | 149 | adantrr 717 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋) | 
| 151 | 150 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋)) | 
| 152 | 151 | ancrd 551 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) | 
| 153 | 152 | eximdv 1916 | . . . . . . . . . . . . . 14
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) | 
| 154 | 153 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) | 
| 155 | 154 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) | 
| 156 | 155 | adantr 480 | . . . . . . . . . . 11
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))) | 
| 157 | 140, 156 | mpd 15 | . . . . . . . . . 10
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))) | 
| 158 |  | df-rex 3070 | . . . . . . . . . 10
⊢
(∃𝑟 ∈
𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))) | 
| 159 | 157, 158 | sylibr 234 | . . . . . . . . 9
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) | 
| 160 | 133, 159 | r19.29a 3161 | . . . . . . . 8
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞) | 
| 161 |  | df-br 5143 | . . . . . . . 8
⊢ (𝑝𝐴𝑞 ↔ 〈𝑝, 𝑞〉 ∈ 𝐴) | 
| 162 | 160, 161 | sylib 218 | . . . . . . 7
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ 𝐴) | 
| 163 | 40, 41, 42, 43, 162 | syl31anc 1374 | . . . . . 6
⊢
(((((((𝑋 ≠
∅ ∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 〈𝑝, 𝑞〉 ∈ 𝐴) | 
| 164 | 39, 163 | mpdan 687 | . . . . 5
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 〈𝑝, 𝑞〉 ∈ 𝐴) | 
| 165 | 164 | ex 412 | . . . 4
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (〈𝑝, 𝑞〉 ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) → 〈𝑝, 𝑞〉 ∈ 𝐴)) | 
| 166 | 19, 165 | relssdv 5797 | . . 3
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) | 
| 167 |  | id 22 | . . . . . 6
⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2)))) | 
| 168 | 167, 167 | coeq12d 5874 | . . . . 5
⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) | 
| 169 | 168 | sseq1d 4014 | . . . 4
⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)) | 
| 170 | 169 | rspcev 3621 | . . 3
⊢ (((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) | 
| 171 | 17, 166, 170 | syl2anc 584 | . 2
⊢
(((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) | 
| 172 | 9 | metustel 24564 | . . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) | 
| 173 | 172 | adantl 481 | . . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))) | 
| 174 | 173 | biimpa 476 | . 2
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))) | 
| 175 | 171, 174 | r19.29a 3161 | 1
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) |