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

Theorem metustexhalf 22558
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 827 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2 simplr 809 . . . . . 6 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
32rphalfcld 12073 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ+)
4 eqidd 2757 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2))))
5 oveq2 6817 . . . . . . . 8 (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
65imaeq2d 5620 . . . . . . 7 (𝑏 = (𝑎 / 2) → (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)(𝑎 / 2))))
76eqeq2d 2766 . . . . . 6 (𝑏 = (𝑎 / 2) → ((𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)) ↔ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2)))))
87rspcev 3445 . . . . 5 (((𝑎 / 2) ∈ ℝ+ ∧ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)))
93, 4, 8syl2anc 696 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)))
10 metust.1 . . . . . . 7 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
11 oveq2 6817 . . . . . . . . . 10 (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
1211imaeq2d 5620 . . . . . . . . 9 (𝑎 = 𝑏 → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)𝑏)))
1312cbvmptv 4898 . . . . . . . 8 (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1413rneqi 5503 . . . . . . 7 ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1510, 14eqtri 2778 . . . . . 6 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1615metustel 22552 . . . . 5 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))))
1716biimpar 503 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
181, 9, 17syl2anc 696 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
19 relco 5790 . . . . 5 Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))
2019a1i 11 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
21 cossxp 5815 . . . . . . . . . 10 ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2))))
22 cnvimass 5639 . . . . . . . . . . . . . 14 (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
23 psmetf 22308 . . . . . . . . . . . . . . 15 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
24 fdm 6208 . . . . . . . . . . . . . . 15 (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom 𝐷 = (𝑋 × 𝑋))
2523, 24syl 17 . . . . . . . . . . . . . 14 (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
2622, 25syl5sseq 3790 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
27 dmss 5474 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
28 rnss 5505 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
29 xpss12 5277 . . . . . . . . . . . . . 14 ((dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
3027, 28, 29syl2anc 696 . . . . . . . . . . . . 13 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
3126, 30syl 17 . . . . . . . . . . . 12 (𝐷 ∈ (PsMet‘𝑋) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
3231adantl 473 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
33 dmxp 5495 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
34 rnxp 5718 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
3533, 34xpeq12d 5293 . . . . . . . . . . . 12 (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3635adantr 472 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3732, 36sseqtrd 3778 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3821, 37syl5ss 3751 . . . . . . . . 9 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3938ad3antrrr 768 . . . . . . . 8 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
4039sselda 3740 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
41 opelxp 5299 . . . . . . 7 (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝𝑋𝑞𝑋))
4240, 41sylib 208 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝𝑋𝑞𝑋))
43 simpll 807 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))))
44 simprl 811 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑝𝑋)
45 simprr 813 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑞𝑋)
46 simplr 809 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
47 simplll 815 . . . . . . . . . . . . . . 15 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋))
4847simp1d 1137 . . . . . . . . . . . . . 14 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))))
4948, 1syl 17 . . . . . . . . . . . . 13 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
5048, 2syl 17 . . . . . . . . . . . . 13 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
5149, 50jca 555 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
5247simp2d 1138 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
5347simp3d 1139 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
5451, 52, 533jca 1123 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
55 simplr 809 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
56 simprl 811 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
57 simprr 813 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
58 simpll 807 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
5958simp1d 1137 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
6059simpld 477 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
61 ffun 6205 . . . . . . . . . . . . . 14 (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun 𝐷)
6223, 61syl 17 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
6360, 62syl 17 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
6458simp2d 1138 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
6558simp3d 1139 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
6664, 65, 41sylanbrc 701 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
6760, 25syl 17 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
6866, 67eleqtrrd 2838 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
69 0xr 10274 . . . . . . . . . . . . . 14 0 ∈ ℝ*
7069a1i 11 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ*)
7159simprd 482 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
7271rpxrd 12062 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*)
7360, 23syl 17 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
7473, 66ffvelrnd 6519 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ*)
75 psmetge0 22314 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝𝑋𝑞𝑋) → 0 ≤ (𝑝𝐷𝑞))
7660, 64, 65, 75syl3anc 1477 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
77 df-ov 6812 . . . . . . . . . . . . . 14 (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
7876, 77syl6breq 4841 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
7977, 74syl5eqel 2839 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ*)
80 0red 10229 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
8171rpred 12061 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
8281rehalfcld 11467 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
8382rexrd 10277 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ*)
84 df-ov 6812 . . . . . . . . . . . . . . . . . . . 20 (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
85 simplr 809 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
86 opelxp 5299 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝𝑋𝑟𝑋))
8764, 85, 86sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
8887, 67eleqtrrd 2838 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
89 simprl 811 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
90 df-br 4801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
9189, 90sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
92 fvimacnv 6491 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
9392biimpar 503 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9463, 88, 91, 93syl21anc 1476 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9584, 94syl5eqel 2839 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
96 elico2 12426 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
9796biimpa 502 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
9897simp1d 1137 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
9980, 83, 95, 98syl21anc 1476 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
100 df-ov 6812 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
101 opelxp 5299 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑟𝑋𝑞𝑋))
10285, 65, 101sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
103102, 67eleqtrrd 2838 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
104 simprr 813 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
105 df-br 4801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
106104, 105sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
107 fvimacnv 6491 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
108107biimpar 503 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
10963, 103, 106, 108syl21anc 1476 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
110100, 109syl5eqel 2839 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
111 elico2 12426 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
112111biimpa 502 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
113112simp1d 1137 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
11480, 83, 110, 113syl21anc 1476 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
115 rexadd 12252 . . . . . . . . . . . . . . . . . 18 (((𝑝𝐷𝑟) ∈ ℝ ∧ (𝑟𝐷𝑞) ∈ ℝ) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
11699, 114, 115syl2anc 696 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
11799, 114readdcld 10257 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
118116, 117eqeltrd 2835 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
119118rexrd 10277 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ*)
120 psmettri 22313 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝𝑋𝑞𝑋𝑟𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
12160, 64, 65, 85, 120syl13anc 1479 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
12297simp3d 1139 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
12380, 83, 95, 122syl21anc 1476 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
124112simp3d 1139 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
12580, 83, 110, 124syl21anc 1476 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
12699, 114, 81, 123, 125lt2halvesd 11468 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
127116, 126eqbrtrd 4822 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎)
12879, 119, 72, 121, 127xrlelttrd 12180 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
12977, 128syl5eqbrr 4836 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
130 elico1 12407 . . . . . . . . . . . . . 14 ((0 ∈ ℝ*𝑎 ∈ ℝ*) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ((𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ* ∧ 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩) ∧ (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)))
131130biimpar 503 . . . . . . . . . . . . 13 (((0 ∈ ℝ*𝑎 ∈ ℝ*) ∧ ((𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ* ∧ 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩) ∧ (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
13270, 72, 74, 78, 129, 131syl23anc 1484 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
133 fvimacnv 6491 . . . . . . . . . . . . . 14 ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎))))
134133biimpa 502 . . . . . . . . . . . . 13 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
135 df-br 4801 . . . . . . . . . . . . 13 (𝑝(𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
136134, 135sylibr 224 . . . . . . . . . . . 12 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13763, 68, 132, 136syl21anc 1476 . . . . . . . . . . 11 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13854, 55, 56, 57, 137syl22anc 1478 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13948simprd 482 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (𝐷 “ (0[,)𝑎)))
140139breqd 4811 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞𝑝(𝐷 “ (0[,)𝑎))𝑞))
141138, 140mpbird 247 . . . . . . . . 9 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞)
142 simpr 479 . . . . . . . . . . . . 13 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
143 df-br 4801 . . . . . . . . . . . . 13 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
144142, 143sylibr 224 . . . . . . . . . . . 12 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞)
145 vex 3339 . . . . . . . . . . . . 13 𝑝 ∈ V
146 vex 3339 . . . . . . . . . . . . 13 𝑞 ∈ V
147145, 146brco 5444 . . . . . . . . . . . 12 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
148144, 147sylib 208 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
14926adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
150149, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
15134adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
152150, 151sseqtrd 3778 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
153152adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
154 vex 3339 . . . . . . . . . . . . . . . . . . . . 21 𝑟 ∈ V
155145, 154brelrn 5507 . . . . . . . . . . . . . . . . . . . 20 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
156155adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
157153, 156sseldd 3741 . . . . . . . . . . . . . . . . . 18 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟𝑋)
158157adantrr 755 . . . . . . . . . . . . . . . . 17 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
159158ex 449 . . . . . . . . . . . . . . . 16 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟𝑋))
160159ancrd 578 . . . . . . . . . . . . . . 15 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
161160eximdv 1991 . . . . . . . . . . . . . 14 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
162161ad3antrrr 768 . . . . . . . . . . . . 13 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
1631623ad2ant1 1128 . . . . . . . . . . . 12 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
164163adantr 472 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
165148, 164mpd 15 . . . . . . . . . 10 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
166 df-rex 3052 . . . . . . . . . 10 (∃𝑟𝑋 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
167165, 166sylibr 224 . . . . . . . . 9 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟𝑋 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
168141, 167r19.29a 3212 . . . . . . . 8 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
169 df-br 4801 . . . . . . . 8 (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
170168, 169sylib 208 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
17143, 44, 45, 46, 170syl31anc 1480 . . . . . 6 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
17242, 171mpdan 705 . . . . 5 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
173172ex 449 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
17420, 173relssdv 5365 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
175 id 22 . . . . . 6 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (𝐷 “ (0[,)(𝑎 / 2))))
176175, 175coeq12d 5438 . . . . 5 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → (𝑣𝑣) = ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
177176sseq1d 3769 . . . 4 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣𝑣) ⊆ 𝐴 ↔ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
178177rspcev 3445 . . 3 (((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
17918, 174, 178syl2anc 696 . 2 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
18010metustel 22552 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
181180adantl 473 . . 3 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
182181biimpa 502 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎)))
183179, 182r19.29a 3212 1 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1628  wex 1849  wcel 2135  wne 2928  wrex 3047  wss 3711  c0 4054  cop 4323   class class class wbr 4800  cmpt 4877   × cxp 5260  ccnv 5261  dom cdm 5262  ran crn 5263  cima 5265  ccom 5266  Rel wrel 5267  Fun wfun 6039  wf 6041  cfv 6045  (class class class)co 6809  cr 10123  0cc0 10124   + caddc 10127  *cxr 10261   < clt 10262  cle 10263   / cdiv 10872  2c2 11258  +crp 12021   +𝑒 cxad 12133  [,)cico 12366  PsMetcpsmet 19928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-po 5183  df-so 5184  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-1st 7329  df-2nd 7330  df-er 7907  df-map 8021  df-en 8118  df-dom 8119  df-sdom 8120  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-2 11267  df-rp 12022  df-xneg 12135  df-xadd 12136  df-xmul 12137  df-ico 12370  df-psmet 19936
This theorem is referenced by:  metust  22560
  Copyright terms: Public domain W3C validator