Theorem metustexhalf 24500

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.

Step	Hyp	Ref	Expression
1		simp-4r 783	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2		simplr 768	. . . . . 6 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
3	2	rphalfcld 12961	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ+)
4		eqidd 2737	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2))))
5		oveq2 7366	. . . . . . 7 ⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
6	5	imaeq2d 6019	. . . . . 6 ⊢ (𝑏 = (𝑎 / 2) → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)(𝑎 / 2))))
7	6	rspceeqv 3599	. . . . 5 ⊢ (((𝑎 / 2) ∈ ℝ+ ∧ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)))
8	3, 4, 7	syl2anc 584	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)))
9		metust.1	. . . . . . 7 ⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))
10		oveq2 7366	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
11	10	imaeq2d 6019	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑏)))
12	11	cbvmptv 5202	. . . . . . . 8 ⊢ (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))
13	12	rneqi 5886	. . . . . . 7 ⊢ ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))
14	9, 13	eqtri 2759	. . . . . 6 ⊢ 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))
15	14	metustel 24494	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))))
16	15	biimpar 477	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
17	1, 8, 16	syl2anc 584	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18		relco 6067	. . . . 5 ⊢ Rel ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))
19	18	a1i 11	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → Rel ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
20		cossxp 6230	. . . . . . . . . 10 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2))))
21		cnvimass 6041	. . . . . . . . . . . . . 14 ⊢ (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22		psmetf 24250	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
23	21, 22	fssdm 6681	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24		dmss 5851	. . . . . . . . . . . . . 14 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25		rnss 5888	. . . . . . . . . . . . . 14 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26		xpss12 5639	. . . . . . . . . . . . . 14 ⊢ ((dom (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
27	24, 25, 26	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
28	23, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
29	28	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30		dmxp 5878	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31		rnxp 6128	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
32	30, 31	xpeq12d 5655	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
33	32	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
34	29, 33	sseqtrd 3970	. . . . . . . . . 10 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
35	20, 34	sstrid 3945	. . . . . . . . 9 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
36	35	ad3antrrr 730	. . . . . . . 8 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
37	36	sselda 3933	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38		opelxp 5660	. . . . . . 7 ⊢ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
39	37, 38	sylib 218	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
40		simpll 766	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
41		simprl 770	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑝 ∈ 𝑋)
42		simprr 772	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑞 ∈ 𝑋)
43		simplr 768	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
44		simplll 774	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
45	44	simp1d 1142	. . . . . . . . . . . . . 14 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
46	45, 1	syl 17	. . . . . . . . . . . . 13 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
47	45, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
48	46, 47	jca 511	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
49	44	simp2d 1143	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
50	44	simp3d 1144	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
51	48, 49, 50	3jca 1128	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
52		simplr 768	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
53		simprl 770	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
54		simprr 772	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
55		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
56	55	simp1d 1142	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
57	56	simpld 494	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
58	22	ffund 6666	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
59	57, 58	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
60	55	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
61	55	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
62	60, 61	opelxpd 5663	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
63	22	fdmd 6672	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
64	57, 63	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
65	62, 64	eleqtrrd 2839	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66		0xr 11179	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ*
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ*)
68	56	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
69	68	rpxrd 12950	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*)
70	57, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
71	70, 62	ffvelcdmd 7030	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ*)
72		psmetge0 24256	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞))
73	57, 60, 61, 72	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74		df-ov 7361	. . . . . . . . . . . . . 14 ⊢ (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
75	73, 74	breqtrdi 5139	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
76	74, 71	eqeltrid 2840	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ*)
77		0red 11135	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
78	68	rpred 12949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
79	78	rehalfcld 12388	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
80	79	rexrd 11182	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ*)
81		df-ov 7361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
83	60, 82	opelxpd 5663	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
84	83, 64	eleqtrrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85		simprl 770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86		df-br 5099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
87	85, 86	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
88		fvimacnv 6998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))))
89	88	biimpar 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
90	59, 84, 87, 89	syl21anc 837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
91	81, 90	eqeltrid 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92		elico2 13326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
93	92	biimpa 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
94	93	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
95	77, 80, 91, 94	syl21anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96		df-ov 7361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
97	82, 61	opelxpd 5663	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
98	97, 64	eleqtrrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100		df-br 5099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
101	99, 100	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
102		fvimacnv 6998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))))
103	102	biimpar 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
104	59, 98, 101, 103	syl21anc 837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
105	96, 104	eqeltrid 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106		elico2 13326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107	106	biimpa 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108	107	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
109	77, 80, 105, 108	syl21anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
110	95, 109	rexaddd 13149	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
111	95, 109	readdcld 11161	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112	110, 111	eqeltrd 2836	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113	112	rexrd 11182	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ*)
114		psmettri 24255	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
115	57, 60, 61, 82, 114	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
116	93	simp3d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
117	77, 80, 91, 116	syl21anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118	107	simp3d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
119	77, 80, 105, 118	syl21anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
120	95, 109, 78, 117, 119	lt2halvesd 12389	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121	110, 120	eqbrtrd 5120	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎)
122	76, 113, 69, 115, 121	xrlelttrd 13074	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
123	74, 122	eqbrtrrid 5134	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
124	67, 69, 71, 75, 123	elicod 13311	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125		fvimacnv 6998	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (◡𝐷 “ (0[,)𝑎))))
126	125	biimpa 476	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (◡𝐷 “ (0[,)𝑎)))
127		df-br 5099	. . . . . . . . . . . . 13 ⊢ (𝑝(◡𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (◡𝐷 “ (0[,)𝑎)))
128	126, 127	sylibr 234	. . . . . . . . . . . 12 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)
129	59, 65, 124, 128	syl21anc 837	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)
130	51, 52, 53, 54, 129	syl22anc 838	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)
131	45	simprd 495	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (◡𝐷 “ (0[,)𝑎)))
132	131	breqd 5109	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞 ↔ 𝑝(◡𝐷 “ (0[,)𝑎))𝑞))
133	130, 132	mpbird 257	. . . . . . . . 9 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞)
134		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
135		df-br 5099	. . . . . . . . . . . . 13 ⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
136	134, 135	sylibr 234	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞)
137		vex 3444	. . . . . . . . . . . . 13 ⊢ 𝑝 ∈ V
138		vex 3444	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
139	137, 138	brco 5819	. . . . . . . . . . . 12 ⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140	136, 139	sylib 218	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
141	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
142	141, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
143	31	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
144	142, 143	sseqtrd 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145	144	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
146		vex 3444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑟 ∈ V
147	137, 146	brelrn 5891	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2))))
148	147	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2))))
149	145, 148	sseldd 3934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋)
150	149	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
151	150	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋))
152	151	ancrd 551	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
153	152	eximdv 1918	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
154	153	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
155	154	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156	155	adantr 480	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
157	140, 156	mpd 15	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
158		df-rex 3061	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
159	157, 158	sylibr 234	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
160	133, 159	r19.29a 3144	. . . . . . . 8 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
161		df-br 5099	. . . . . . . 8 ⊢ (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162	160, 161	sylib 218	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
163	40, 41, 42, 43, 162	syl31anc 1375	. . . . . 6 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
164	39, 163	mpdan 687	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
165	164	ex 412	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
166	19, 165	relssdv 5737	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
167		id 22	. . . . . 6 ⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))))
168	167, 167	coeq12d 5813	. . . . 5 ⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
169	168	sseq1d 3965	. . . 4 ⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
170	169	rspcev 3576	. . 3 ⊢ (((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
171	17, 166, 170	syl2anc 584	. 2 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
172	9	metustel 24494	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
173	172	adantl 481	. . 3 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
174	173	biimpa 476	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))
175	171, 174	r19.29a 3144	1 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∃wrex 3060   ⊆ wss 3901  ∅c0 4285  ⟨cop 4586   class class class wbr 5098   ↦ cmpt 5179   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   “ cima 5627   ∘ ccom 5628  Rel wrel 5629  Fun wfun 6486  ⟶wf 6488  ‘cfv 6492  (class class class)co 7358  ℝcr 11025  0cc0 11026   + caddc 11029  ℝ^*cxr 11165   < clt 11166   ≤ cle 11167   / cdiv 11794  2c2 12200  ℝ⁺crp 12905   +_𝑒 cxad 13024  [,)cico 13263  PsMetcpsmet 21293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-map 8765  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-2 12208  df-rp 12906  df-xneg 13026  df-xadd 13027  df-xmul 13028  df-ico 13267  df-psmet 21301

This theorem is referenced by:  metust  24502