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

Theorem metustexhalf 24585
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 784 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2 simplr 769 . . . . . 6 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
32rphalfcld 13087 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ+)
4 eqidd 2736 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2))))
5 oveq2 7439 . . . . . . 7 (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
65imaeq2d 6080 . . . . . 6 (𝑏 = (𝑎 / 2) → (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)(𝑎 / 2))))
76rspceeqv 3645 . . . . 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 7439 . . . . . . . . . 10 (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
1110imaeq2d 6080 . . . . . . . . 9 (𝑎 = 𝑏 → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)𝑏)))
1211cbvmptv 5261 . . . . . . . 8 (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1312rneqi 5951 . . . . . . 7 ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
149, 13eqtri 2763 . . . . . 6 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1514metustel 24579 . . . . 5 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))))
1615biimpar 477 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
171, 8, 16syl2anc 584 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18 relco 6129 . . . . 5 Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))
1918a1i 11 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
20 cossxp 6294 . . . . . . . . . 10 ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2))))
21 cnvimass 6102 . . . . . . . . . . . . . 14 (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22 psmetf 24332 . . . . . . . . . . . . . 14 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
2321, 22fssdm 6756 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24 dmss 5916 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25 rnss 5953 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26 xpss12 5704 . . . . . . . . . . . . . 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 481 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30 dmxp 5942 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31 rnxp 6192 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
3230, 31xpeq12d 5720 . . . . . . . . . . . 12 (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3332adantr 480 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3429, 33sseqtrd 4036 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3520, 34sstrid 4007 . . . . . . . . 9 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3635ad3antrrr 730 . . . . . . . 8 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3736sselda 3995 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38 opelxp 5725 . . . . . . 7 (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝𝑋𝑞𝑋))
3937, 38sylib 218 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝𝑋𝑞𝑋))
40 simpll 767 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))))
41 simprl 771 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑝𝑋)
42 simprr 773 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑞𝑋)
43 simplr 769 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
44 simplll 775 . . . . . . . . . . . . . . 15 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋))
4544simp1d 1141 . . . . . . . . . . . . . 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 511 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
4944simp2d 1142 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
5044simp3d 1143 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
5148, 49, 503jca 1127 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
52 simplr 769 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
53 simprl 771 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
54 simprr 773 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
55 simpll 767 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
5655simp1d 1141 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
5756simpld 494 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
5822ffund 6741 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
5957, 58syl 17 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
6055simp2d 1142 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
6155simp3d 1143 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
6260, 61opelxpd 5728 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
6322fdmd 6747 . . . . . . . . . . . . . 14 (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
6457, 63syl 17 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
6562, 64eleqtrrd 2842 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66 0xr 11306 . . . . . . . . . . . . . 14 0 ∈ ℝ*
6766a1i 11 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ*)
6856simprd 495 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
6968rpxrd 13076 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*)
7057, 22syl 17 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
7170, 62ffvelcdmd 7105 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ*)
72 psmetge0 24338 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝𝑋𝑞𝑋) → 0 ≤ (𝑝𝐷𝑞))
7357, 60, 61, 72syl3anc 1370 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74 df-ov 7434 . . . . . . . . . . . . . 14 (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
7573, 74breqtrdi 5189 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
7674, 71eqeltrid 2843 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ*)
77 0red 11262 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
7868rpred 13075 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
7978rehalfcld 12511 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
8079rexrd 11309 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ*)
81 df-ov 7434 . . . . . . . . . . . . . . . . . . . 20 (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82 simplr 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
8360, 82opelxpd 5728 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
8483, 64eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85 simprl 771 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86 df-br 5149 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
8785, 86sylib 218 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
88 fvimacnv 7073 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
8988biimpar 477 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9059, 84, 87, 89syl21anc 838 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9181, 90eqeltrid 2843 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92 elico2 13448 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
9392biimpa 476 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
9493simp1d 1141 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
9577, 80, 91, 94syl21anc 838 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96 df-ov 7434 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
9782, 61opelxpd 5728 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
9897, 64eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99 simprr 773 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100 df-br 5149 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
10199, 100sylib 218 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
102 fvimacnv 7073 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
103102biimpar 477 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
10459, 98, 101, 103syl21anc 838 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
10596, 104eqeltrid 2843 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106 elico2 13448 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107106biimpa 476 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108107simp1d 1141 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
10977, 80, 105, 108syl21anc 838 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
11095, 109rexaddd 13273 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
11195, 109readdcld 11288 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112110, 111eqeltrd 2839 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113112rexrd 11309 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ*)
114 psmettri 24337 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝𝑋𝑞𝑋𝑟𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
11557, 60, 61, 82, 114syl13anc 1371 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
11693simp3d 1143 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
11777, 80, 91, 116syl21anc 838 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118107simp3d 1143 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
11977, 80, 105, 118syl21anc 838 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
12095, 109, 78, 117, 119lt2halvesd 12512 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121110, 120eqbrtrd 5170 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎)
12276, 113, 69, 115, 121xrlelttrd 13199 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
12374, 122eqbrtrrid 5184 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
12467, 69, 71, 75, 123elicod 13434 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125 fvimacnv 7073 . . . . . . . . . . . . . 14 ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎))))
126125biimpa 476 . . . . . . . . . . . . 13 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
127 df-br 5149 . . . . . . . . . . . . 13 (𝑝(𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
128126, 127sylibr 234 . . . . . . . . . . . 12 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
12959, 65, 124, 128syl21anc 838 . . . . . . . . . . 11 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13051, 52, 53, 54, 129syl22anc 839 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13145simprd 495 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (𝐷 “ (0[,)𝑎)))
132131breqd 5159 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞𝑝(𝐷 “ (0[,)𝑎))𝑞))
133130, 132mpbird 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 5149 . . . . . . . . . . . . 13 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
136134, 135sylibr 234 . . . . . . . . . . . 12 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞)
137 vex 3482 . . . . . . . . . . . . 13 𝑝 ∈ V
138 vex 3482 . . . . . . . . . . . . 13 𝑞 ∈ V
139137, 138brco 5884 . . . . . . . . . . . 12 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140136, 139sylib 218 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
14123adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
142141, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
14331adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
144142, 143sseqtrd 4036 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145144adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
146 vex 3482 . . . . . . . . . . . . . . . . . . . . 21 𝑟 ∈ V
147137, 146brelrn 5956 . . . . . . . . . . . . . . . . . . . 20 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
148147adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
149145, 148sseldd 3996 . . . . . . . . . . . . . . . . . 18 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟𝑋)
150149adantrr 717 . . . . . . . . . . . . . . . . 17 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
151150ex 412 . . . . . . . . . . . . . . . 16 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟𝑋))
152151ancrd 551 . . . . . . . . . . . . . . 15 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
153152eximdv 1915 . . . . . . . . . . . . . 14 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
154153ad3antrrr 730 . . . . . . . . . . . . 13 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
1551543ad2ant1 1132 . . . . . . . . . . . 12 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156155adantr 480 . . . . . . . . . . 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 3069 . . . . . . . . . 10 (∃𝑟𝑋 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
159157, 158sylibr 234 . . . . . . . . 9 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟𝑋 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
160133, 159r19.29a 3160 . . . . . . . 8 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
161 df-br 5149 . . . . . . . 8 (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162160, 161sylib 218 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
16340, 41, 42, 43, 162syl31anc 1372 . . . . . 6 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
16439, 163mpdan 687 . . . . 5 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
165164ex 412 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
16619, 165relssdv 5801 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
167 id 22 . . . . . 6 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (𝐷 “ (0[,)(𝑎 / 2))))
168167, 167coeq12d 5878 . . . . 5 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → (𝑣𝑣) = ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
169168sseq1d 4027 . . . 4 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣𝑣) ⊆ 𝐴 ↔ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
170169rspcev 3622 . . 3 (((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
17117, 166, 170syl2anc 584 . 2 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
1729metustel 24579 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
173172adantl 481 . . 3 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
174173biimpa 476 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎)))
175171, 174r19.29a 3160 1 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wex 1776  wcel 2106  wne 2938  wrex 3068  wss 3963  c0 4339  cop 4637   class class class wbr 5148  cmpt 5231   × cxp 5687  ccnv 5688  dom cdm 5689  ran crn 5690  cima 5692  ccom 5693  Rel wrel 5694  Fun wfun 6557  wf 6559  cfv 6563  (class class class)co 7431  cr 11152  0cc0 11153   + caddc 11156  *cxr 11292   < clt 11293  cle 11294   / cdiv 11918  2c2 12319  +crp 13032   +𝑒 cxad 13150  [,)cico 13386  PsMetcpsmet 21366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-2 12327  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ico 13390  df-psmet 21374
This theorem is referenced by:  metust  24587
  Copyright terms: Public domain W3C validator