MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metustexhalf Structured version   Visualization version   GIF version

Theorem metustexhalf 23912
Description: For any element 𝐴 of the filter base generated by the metric 𝐷, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
metust.1 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
Assertion
Ref Expression
metustexhalf (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
Distinct variable groups:   𝐷,𝑎   𝑋,𝑎   𝐴,𝑎   𝐹,𝑎,𝑣   𝑣,𝐴   𝑣,𝐷   𝑣,𝐹   𝑣,𝑋

Proof of Theorem metustexhalf
Dummy variables 𝑏 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp-4r 782 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2 simplr 767 . . . . . 6 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
32rphalfcld 12969 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ+)
4 eqidd 2737 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2))))
5 oveq2 7365 . . . . . . 7 (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
65imaeq2d 6013 . . . . . 6 (𝑏 = (𝑎 / 2) → (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)(𝑎 / 2))))
76rspceeqv 3595 . . . . 5 (((𝑎 / 2) ∈ ℝ+ ∧ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)))
83, 4, 7syl2anc 584 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)))
9 metust.1 . . . . . . 7 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
10 oveq2 7365 . . . . . . . . . 10 (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
1110imaeq2d 6013 . . . . . . . . 9 (𝑎 = 𝑏 → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)𝑏)))
1211cbvmptv 5218 . . . . . . . 8 (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1312rneqi 5892 . . . . . . 7 ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
149, 13eqtri 2764 . . . . . 6 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1514metustel 23906 . . . . 5 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))))
1615biimpar 478 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
171, 8, 16syl2anc 584 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18 relco 6060 . . . . 5 Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))
1918a1i 11 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
20 cossxp 6224 . . . . . . . . . 10 ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2))))
21 cnvimass 6033 . . . . . . . . . . . . . 14 (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22 psmetf 23659 . . . . . . . . . . . . . 14 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
2321, 22fssdm 6688 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24 dmss 5858 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25 rnss 5894 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26 xpss12 5648 . . . . . . . . . . . . . 14 ((dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
2724, 25, 26syl2anc 584 . . . . . . . . . . . . 13 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
2823, 27syl 17 . . . . . . . . . . . 12 (𝐷 ∈ (PsMet‘𝑋) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
2928adantl 482 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30 dmxp 5884 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31 rnxp 6122 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
3230, 31xpeq12d 5664 . . . . . . . . . . . 12 (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3332adantr 481 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3429, 33sseqtrd 3984 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3520, 34sstrid 3955 . . . . . . . . 9 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3635ad3antrrr 728 . . . . . . . 8 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3736sselda 3944 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38 opelxp 5669 . . . . . . 7 (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝𝑋𝑞𝑋))
3937, 38sylib 217 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝𝑋𝑞𝑋))
40 simpll 765 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))))
41 simprl 769 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑝𝑋)
42 simprr 771 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑞𝑋)
43 simplr 767 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
44 simplll 773 . . . . . . . . . . . . . . 15 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋))
4544simp1d 1142 . . . . . . . . . . . . . 14 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))))
4645, 1syl 17 . . . . . . . . . . . . 13 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
4745, 2syl 17 . . . . . . . . . . . . 13 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
4846, 47jca 512 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
4944simp2d 1143 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
5044simp3d 1144 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
5148, 49, 503jca 1128 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
52 simplr 767 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
53 simprl 769 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
54 simprr 771 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
55 simpll 765 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
5655simp1d 1142 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
5756simpld 495 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
5822ffund 6672 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
5957, 58syl 17 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
6055simp2d 1143 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
6155simp3d 1144 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
6260, 61opelxpd 5671 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
6322fdmd 6679 . . . . . . . . . . . . . 14 (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
6457, 63syl 17 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
6562, 64eleqtrrd 2841 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66 0xr 11202 . . . . . . . . . . . . . 14 0 ∈ ℝ*
6766a1i 11 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ*)
6856simprd 496 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
6968rpxrd 12958 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*)
7057, 22syl 17 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
7170, 62ffvelcdmd 7036 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ*)
72 psmetge0 23665 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝𝑋𝑞𝑋) → 0 ≤ (𝑝𝐷𝑞))
7357, 60, 61, 72syl3anc 1371 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74 df-ov 7360 . . . . . . . . . . . . . 14 (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
7573, 74breqtrdi 5146 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
7674, 71eqeltrid 2842 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ*)
77 0red 11158 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
7868rpred 12957 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
7978rehalfcld 12400 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
8079rexrd 11205 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ*)
81 df-ov 7360 . . . . . . . . . . . . . . . . . . . 20 (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
8360, 82opelxpd 5671 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
8483, 64eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85 simprl 769 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86 df-br 5106 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
8785, 86sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
88 fvimacnv 7003 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
8988biimpar 478 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9059, 84, 87, 89syl21anc 836 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9181, 90eqeltrid 2842 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92 elico2 13328 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
9392biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
9493simp1d 1142 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
9577, 80, 91, 94syl21anc 836 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96 df-ov 7360 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
9782, 61opelxpd 5671 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
9897, 64eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99 simprr 771 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100 df-br 5106 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
10199, 100sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
102 fvimacnv 7003 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
103102biimpar 478 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
10459, 98, 101, 103syl21anc 836 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
10596, 104eqeltrid 2842 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106 elico2 13328 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107106biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108107simp1d 1142 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
10977, 80, 105, 108syl21anc 836 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
11095, 109rexaddd 13153 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
11195, 109readdcld 11184 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112110, 111eqeltrd 2838 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113112rexrd 11205 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ*)
114 psmettri 23664 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝𝑋𝑞𝑋𝑟𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
11557, 60, 61, 82, 114syl13anc 1372 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
11693simp3d 1144 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
11777, 80, 91, 116syl21anc 836 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118107simp3d 1144 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
11977, 80, 105, 118syl21anc 836 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
12095, 109, 78, 117, 119lt2halvesd 12401 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121110, 120eqbrtrd 5127 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎)
12276, 113, 69, 115, 121xrlelttrd 13079 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
12374, 122eqbrtrrid 5141 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
12467, 69, 71, 75, 123elicod 13314 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125 fvimacnv 7003 . . . . . . . . . . . . . 14 ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎))))
126125biimpa 477 . . . . . . . . . . . . 13 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
127 df-br 5106 . . . . . . . . . . . . 13 (𝑝(𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
128126, 127sylibr 233 . . . . . . . . . . . 12 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
12959, 65, 124, 128syl21anc 836 . . . . . . . . . . 11 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13051, 52, 53, 54, 129syl22anc 837 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13145simprd 496 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (𝐷 “ (0[,)𝑎)))
132131breqd 5116 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞𝑝(𝐷 “ (0[,)𝑎))𝑞))
133130, 132mpbird 256 . . . . . . . . 9 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞)
134 simpr 485 . . . . . . . . . . . . 13 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
135 df-br 5106 . . . . . . . . . . . . 13 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
136134, 135sylibr 233 . . . . . . . . . . . 12 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞)
137 vex 3449 . . . . . . . . . . . . 13 𝑝 ∈ V
138 vex 3449 . . . . . . . . . . . . 13 𝑞 ∈ V
139137, 138brco 5826 . . . . . . . . . . . 12 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140136, 139sylib 217 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
14123adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
142141, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
14331adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
144142, 143sseqtrd 3984 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145144adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
146 vex 3449 . . . . . . . . . . . . . . . . . . . . 21 𝑟 ∈ V
147137, 146brelrn 5897 . . . . . . . . . . . . . . . . . . . 20 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
148147adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
149145, 148sseldd 3945 . . . . . . . . . . . . . . . . . 18 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟𝑋)
150149adantrr 715 . . . . . . . . . . . . . . . . 17 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
151150ex 413 . . . . . . . . . . . . . . . 16 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟𝑋))
152151ancrd 552 . . . . . . . . . . . . . . 15 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
153152eximdv 1920 . . . . . . . . . . . . . 14 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
154153ad3antrrr 728 . . . . . . . . . . . . 13 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
1551543ad2ant1 1133 . . . . . . . . . . . 12 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156155adantr 481 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
157140, 156mpd 15 . . . . . . . . . 10 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
158 df-rex 3074 . . . . . . . . . 10 (∃𝑟𝑋 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
159157, 158sylibr 233 . . . . . . . . 9 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟𝑋 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
160133, 159r19.29a 3159 . . . . . . . 8 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
161 df-br 5106 . . . . . . . 8 (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162160, 161sylib 217 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
16340, 41, 42, 43, 162syl31anc 1373 . . . . . 6 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
16439, 163mpdan 685 . . . . 5 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
165164ex 413 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
16619, 165relssdv 5744 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
167 id 22 . . . . . 6 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (𝐷 “ (0[,)(𝑎 / 2))))
168167, 167coeq12d 5820 . . . . 5 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → (𝑣𝑣) = ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
169168sseq1d 3975 . . . 4 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣𝑣) ⊆ 𝐴 ↔ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
170169rspcev 3581 . . 3 (((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
17117, 166, 170syl2anc 584 . 2 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
1729metustel 23906 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
173172adantl 482 . . 3 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
174173biimpa 477 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎)))
175171, 174r19.29a 3159 1 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wrex 3073  wss 3910  c0 4282  cop 4592   class class class wbr 5105  cmpt 5188   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cima 5636  ccom 5637  Rel wrel 5638  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  cr 11050  0cc0 11051   + caddc 11054  *cxr 11188   < clt 11189  cle 11190   / cdiv 11812  2c2 12208  +crp 12915   +𝑒 cxad 13031  [,)cico 13266  PsMetcpsmet 20780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-2 12216  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ico 13270  df-psmet 20788
This theorem is referenced by:  metust  23914
  Copyright terms: Public domain W3C validator