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

Theorem metustexhalf 22271
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 806 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2 simplr 791 . . . . . 6 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
32rphalfcld 11828 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ+)
4 eqidd 2622 . . . . 5 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2))))
5 oveq2 6612 . . . . . . . 8 (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
65imaeq2d 5425 . . . . . . 7 (𝑏 = (𝑎 / 2) → (𝐷 “ (0[,)𝑏)) = (𝐷 “ (0[,)(𝑎 / 2))))
76eqeq2d 2631 . . . . . 6 (𝑏 = (𝑎 / 2) → ((𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)) ↔ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2)))))
87rspcev 3295 . . . . 5 (((𝑎 / 2) ∈ ℝ+ ∧ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)))
93, 4, 8syl2anc 692 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏)))
10 metust.1 . . . . . . 7 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎)))
11 oveq2 6612 . . . . . . . . . 10 (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
1211imaeq2d 5425 . . . . . . . . 9 (𝑎 = 𝑏 → (𝐷 “ (0[,)𝑎)) = (𝐷 “ (0[,)𝑏)))
1312cbvmptv 4710 . . . . . . . 8 (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1413rneqi 5312 . . . . . . 7 ran (𝑎 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1510, 14eqtri 2643 . . . . . 6 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (𝐷 “ (0[,)𝑏)))
1615metustel 22265 . . . . 5 (𝐷 ∈ (PsMet‘𝑋) → ((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))))
1716biimpar 502 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+ (𝐷 “ (0[,)(𝑎 / 2))) = (𝐷 “ (0[,)𝑏))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
181, 9, 17syl2anc 692 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
19 relco 5592 . . . . 5 Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))
2019a1i 11 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → Rel ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
21 cossxp 5617 . . . . . . . . . 10 ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2))))
22 cnvimass 5444 . . . . . . . . . . . . . 14 (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
23 psmetf 22021 . . . . . . . . . . . . . . 15 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
24 fdm 6008 . . . . . . . . . . . . . . 15 (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom 𝐷 = (𝑋 × 𝑋))
2523, 24syl 17 . . . . . . . . . . . . . 14 (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
2622, 25syl5sseq 3632 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
27 dmss 5283 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
28 rnss 5314 . . . . . . . . . . . . . 14 ((𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
29 xpss12 5186 . . . . . . . . . . . . . 14 ((dom (𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
3027, 28, 29syl2anc 692 . . . . . . . . . . . . 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 482 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
33 dmxp 5304 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
34 rnxp 5523 . . . . . . . . . . . . 13 (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
3533, 34xpeq12d 5100 . . . . . . . . . . . 12 (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3635adantr 481 . . . . . . . . . . 11 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
3732, 36sseqtrd 3620 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝐷 “ (0[,)(𝑎 / 2))) × ran (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3821, 37syl5ss 3594 . . . . . . . . 9 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
3938ad3antrrr 765 . . . . . . . 8 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
4039sselda 3583 . . . . . . 7 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
41 opelxp 5106 . . . . . . 7 (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝𝑋𝑞𝑋))
4240, 41sylib 208 . . . . . 6 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝𝑋𝑞𝑋))
43 simpll 789 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))))
44 simprl 793 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑝𝑋)
45 simprr 795 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → 𝑞𝑋)
46 simplr 791 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
47 simplll 797 . . . . . . . . . . . . . . 15 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋))
4847simp1d 1071 . . . . . . . . . . . . . 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 554 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
5247simp2d 1072 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
5347simp3d 1073 . . . . . . . . . . . 12 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
5451, 52, 533jca 1240 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
55 simplr 791 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
56 simprl 793 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
57 simprr 795 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
58 simpll 789 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋))
5958simp1d 1071 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
6059simpld 475 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
61 ffun 6005 . . . . . . . . . . . . . 14 (𝐷:(𝑋 × 𝑋)⟶ℝ* → Fun 𝐷)
6223, 61syl 17 . . . . . . . . . . . . 13 (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
6360, 62syl 17 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
6458simp2d 1072 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝑋)
6558simp3d 1073 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞𝑋)
6664, 65, 41sylanbrc 697 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
6760, 25syl 17 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
6866, 67eleqtrrd 2701 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
69 0xr 10030 . . . . . . . . . . . . . 14 0 ∈ ℝ*
7069a1i 11 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ*)
7159simprd 479 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
7271rpxrd 11817 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*)
7360, 23syl 17 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
7473, 66ffvelrnd 6316 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ*)
75 psmetge0 22027 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝𝑋𝑞𝑋) → 0 ≤ (𝑝𝐷𝑞))
7660, 64, 65, 75syl3anc 1323 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
77 df-ov 6607 . . . . . . . . . . . . . 14 (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
7876, 77syl6breq 4654 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
7977, 74syl5eqel 2702 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ*)
80 0red 9985 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
8171rpred 11816 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
8281rehalfcld 11223 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
8382rexrd 10033 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ*)
84 df-ov 6607 . . . . . . . . . . . . . . . . . . . 20 (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
85 simplr 791 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
86 opelxp 5106 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝𝑋𝑟𝑋))
8764, 85, 86sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
8887, 67eleqtrrd 2701 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
89 simprl 793 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟)
90 df-br 4614 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
9189, 90sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
92 fvimacnv 6288 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
9392biimpar 502 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9463, 88, 91, 93syl21anc 1322 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
9584, 94syl5eqel 2702 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
96 elico2 12179 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
9796biimpa 501 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
9897simp1d 1071 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
9980, 83, 95, 98syl21anc 1322 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
100 df-ov 6607 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
101 opelxp 5106 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑟𝑋𝑞𝑋))
10285, 65, 101sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
103102, 67eleqtrrd 2701 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
104 simprr 795 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)
105 df-br 4614 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
106104, 105sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2))))
107 fvimacnv 6288 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))))
108107biimpar 502 . . . . . . . . . . . . . . . . . . . . 21 (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
10963, 103, 106, 108syl21anc 1322 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
110100, 109syl5eqel 2702 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
111 elico2 12179 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
112111biimpa 501 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
113112simp1d 1071 . . . . . . . . . . . . . . . . . . 19 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
11480, 83, 110, 113syl21anc 1322 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
115 rexadd 12006 . . . . . . . . . . . . . . . . . 18 (((𝑝𝐷𝑟) ∈ ℝ ∧ (𝑟𝐷𝑞) ∈ ℝ) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
11699, 114, 115syl2anc 692 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
11799, 114readdcld 10013 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
118116, 117eqeltrd 2698 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
119118rexrd 10033 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ*)
120 psmettri 22026 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝𝑋𝑞𝑋𝑟𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
12160, 64, 65, 85, 120syl13anc 1325 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
12297simp3d 1073 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
12380, 83, 95, 122syl21anc 1322 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
124112simp3d 1073 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
12580, 83, 110, 124syl21anc 1322 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
12699, 114, 81, 123, 125lt2halvesd 11224 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
127116, 126eqbrtrd 4635 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎)
12879, 119, 72, 121, 127xrlelttrd 11935 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
12977, 128syl5eqbrr 4649 . . . . . . . . . . . . 13 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
130 elico1 12160 . . . . . . . . . . . . . 14 ((0 ∈ ℝ*𝑎 ∈ ℝ*) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ((𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ* ∧ 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩) ∧ (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)))
131130biimpar 502 . . . . . . . . . . . . 13 (((0 ∈ ℝ*𝑎 ∈ ℝ*) ∧ ((𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ* ∧ 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩) ∧ (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
13270, 72, 74, 78, 129, 131syl23anc 1330 . . . . . . . . . . . 12 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
133 fvimacnv 6288 . . . . . . . . . . . . . 14 ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎))))
134133biimpa 501 . . . . . . . . . . . . 13 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
135 df-br 4614 . . . . . . . . . . . . 13 (𝑝(𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (𝐷 “ (0[,)𝑎)))
136134, 135sylibr 224 . . . . . . . . . . . 12 (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13763, 68, 132, 136syl21anc 1322 . . . . . . . . . . 11 (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝𝑋𝑞𝑋) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13854, 55, 56, 57, 137syl22anc 1324 . . . . . . . . . 10 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(𝐷 “ (0[,)𝑎))𝑞)
13948simprd 479 . . . . . . . . . . 11 (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟𝑋) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (𝐷 “ (0[,)𝑎)))
140139breqd 4624 . . . . . . . . . 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 477 . . . . . . . . . . . . 13 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
143 df-br 4614 . . . . . . . . . . . . 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 3189 . . . . . . . . . . . . 13 𝑝 ∈ V
146 vex 3189 . . . . . . . . . . . . 13 𝑞 ∈ V
147145, 146brco 5252 . . . . . . . . . . . 12 (𝑝((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
148144, 147sylib 208 . . . . . . . . . . 11 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))
14926adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
150149, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
15134adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
152150, 151sseqtrd 3620 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
153152adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
154 vex 3189 . . . . . . . . . . . . . . . . . . . . 21 𝑟 ∈ V
155145, 154brelrn 5316 . . . . . . . . . . . . . . . . . . . 20 (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
156155adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (𝐷 “ (0[,)(𝑎 / 2))))
157153, 156sseldd 3584 . . . . . . . . . . . . . . . . . 18 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟𝑋)
158157adantrr 752 . . . . . . . . . . . . . . . . 17 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟𝑋)
159158ex 450 . . . . . . . . . . . . . . . 16 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟𝑋))
160159ancrd 576 . . . . . . . . . . . . . . 15 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
161160eximdv 1843 . . . . . . . . . . . . . 14 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
162161ad3antrrr 765 . . . . . . . . . . . . 13 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
1631623ad2ant1 1080 . . . . . . . . . . . 12 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) → (∃𝑟(𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟𝑋 ∧ (𝑝(𝐷 “ (0[,)(𝑎 / 2)))𝑟𝑟(𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
164163adantr 481 . . . . . . . . . . 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 2913 . . . . . . . . . 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 3071 . . . . . . . 8 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
169 df-br 4614 . . . . . . . 8 (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
170168, 169sylib 208 . . . . . . 7 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ 𝑝𝑋𝑞𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
17143, 44, 45, 46, 170syl31anc 1326 . . . . . 6 (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝𝑋𝑞𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
17242, 171mpdan 701 . . . . 5 ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
173172ex 450 . . . 4 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
17420, 173relssdv 5173 . . 3 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
175 id 22 . . . . . 6 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (𝐷 “ (0[,)(𝑎 / 2))))
176175, 175coeq12d 5246 . . . . 5 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → (𝑣𝑣) = ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))))
177176sseq1d 3611 . . . 4 (𝑣 = (𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣𝑣) ⊆ 𝐴 ↔ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
178177rspcev 3295 . . 3 (((𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((𝐷 “ (0[,)(𝑎 / 2))) ∘ (𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
17918, 174, 178syl2anc 692 . 2 (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (𝐷 “ (0[,)𝑎))) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
18010metustel 22265 . . . 4 (𝐷 ∈ (PsMet‘𝑋) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
181180adantl 482 . . 3 ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎))))
182181biimpa 501 . 2 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (𝐷 “ (0[,)𝑎)))
183179, 182r19.29a 3071 1 (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴𝐹) → ∃𝑣𝐹 (𝑣𝑣) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wrex 2908  wss 3555  c0 3891  cop 4154   class class class wbr 4613  cmpt 4673   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cima 5077  ccom 5078  Rel wrel 5079  Fun wfun 5841  wf 5843  cfv 5847  (class class class)co 6604  cr 9879  0cc0 9880   + caddc 9883  *cxr 10017   < clt 10018  cle 10019   / cdiv 10628  2c2 11014  +crp 11776   +𝑒 cxad 11888  [,)cico 12119  PsMetcpsmet 19649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-po 4995  df-so 4996  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-2 11023  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ico 12123  df-psmet 19657
This theorem is referenced by:  metust  22273
  Copyright terms: Public domain W3C validator