Theorem metustexhalf 24674

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 795	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2		simplr 780	. . . . . 6 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ+)
3	2	rphalfcld 13063	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ+)
4		eqidd 2766	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2))))
5		oveq2 7408	. . . . . . 7 ⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
6	5	imaeq2d 6053	. . . . . 6 ⊢ (𝑏 = (𝑎 / 2) → (◡𝐷 “ (0[,)𝑏)) = (◡𝐷 “ (0[,)(𝑎 / 2))))
7	6	rspceeqv 3607	. . . . 5 ⊢ (((𝑎 / 2) ∈ ℝ+ ∧ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)))
8	3, 4, 7	syl2anc 595	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏)))
9		metust.1	. . . . . . 7 ⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))
10		oveq2 7408	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
11	10	imaeq2d 6053	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (◡𝐷 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑏)))
12	11	cbvmptv 5209	. . . . . . . 8 ⊢ (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))
13	12	rneqi 5918	. . . . . . 7 ⊢ ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))
14	9, 13	eqtri 2788	. . . . . 6 ⊢ 𝐹 = ran (𝑏 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑏)))
15	14	metustel 24668	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))))
16	15	biimpar 482	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ+ (◡𝐷 “ (0[,)(𝑎 / 2))) = (◡𝐷 “ (0[,)𝑏))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
17	1, 8, 16	syl2anc 595	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18		relco 6101	. . . . 5 ⊢ Rel ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))
19	18	a1i 11	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → Rel ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
20		cossxp 6263	. . . . . . . . . 10 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2))))
21		cnvimass 6075	. . . . . . . . . . . . . 14 ⊢ (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22		psmetf 24424	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
23	21, 22	fssdm 6715	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24		dmss 5883	. . . . . . . . . . . . . 14 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25		rnss 5920	. . . . . . . . . . . . . 14 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26		xpss12 5667	. . . . . . . . . . . . . 14 ⊢ ((dom (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
27	24, 25, 26	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
28	23, 27	syl 18	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
29	28	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30		dmxp 5910	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31		rnxp 6160	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
32	30, 31	xpeq12d 5683	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
33	32	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
34	29, 33	sseqtrd 3975	. . . . . . . . . 10 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (◡𝐷 “ (0[,)(𝑎 / 2))) × ran (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
35	20, 34	sstrid 3950	. . . . . . . . 9 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
36	35	ad3antrrr 742	. . . . . . . 8 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
37	36	sselda 3939	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38		opelxp 5688	. . . . . . 7 ⊢ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
39	37, 38	sylib 221	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
40		simpll 778	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
41		simprl 782	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑝 ∈ 𝑋)
42		simprr 784	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑞 ∈ 𝑋)
43		simplr 780	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
44		simplll 786	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
45	44	simp1d 1158	. . . . . . . . . . . . . 14 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
46	45, 1	syl 18	. . . . . . . . . . . . 13 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
47	45, 2	syl 18	. . . . . . . . . . . . 13 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
48	46, 47	jca 520	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
49	44	simp2d 1159	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
50	44	simp3d 1160	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
51	48, 49, 50	3jca 1144	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
52		simplr 780	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
53		simprl 782	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
54		simprr 784	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
55		simpll 778	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
56	55	simp1d 1158	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+))
57	56	simpld 499	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
58	22	ffund 6700	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
59	57, 58	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
60	55	simp2d 1159	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
61	55	simp3d 1160	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
62	60, 61	opelxpd 5691	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
63	22	fdmd 6706	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
64	57, 63	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
65	62, 64	eleqtrrd 2868	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66		0xr 11244	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ*
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ*)
68	56	simprd 500	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ+)
69	68	rpxrd 13052	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ*)
70	57, 22	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
71	70, 62	ffvelcdmd 7070	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ*)
72		psmetge0 24430	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞))
73	57, 60, 61, 72	syl3anc 1394	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74		df-ov 7403	. . . . . . . . . . . . . 14 ⊢ (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
75	73, 74	breqtrdi 5146	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
76	74, 71	eqeltrid 2869	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ*)
77		0red 11199	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
78	68	rpred 13051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
79	78	rehalfcld 12482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
80	79	rexrd 11247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ*)
81		df-ov 7403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
83	60, 82	opelxpd 5691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
84	83, 64	eleqtrrd 2868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85		simprl 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86		df-br 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
87	85, 86	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
88		fvimacnv 7038	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))))
89	88	biimpar 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
90	59, 84, 87, 89	syl21anc 850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
91	81, 90	eqeltrid 2869	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92		elico2 13428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
93	92	biimpa 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
94	93	simp1d 1158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
95	77, 80, 91, 94	syl21anc 850	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96		df-ov 7403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
97	82, 61	opelxpd 5691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
98	97, 64	eleqtrrd 2868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99		simprr 784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100		df-br 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
101	99, 100	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2))))
102		fvimacnv 7038	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))))
103	102	biimpar 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
104	59, 98, 101, 103	syl21anc 850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
105	96, 104	eqeltrid 2869	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106		elico2 13428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107	106	biimpa 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108	107	simp1d 1158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
109	77, 80, 105, 108	syl21anc 850	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
110	95, 109	rexaddd 13251	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
111	95, 109	readdcld 11226	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112	110, 111	eqeltrd 2865	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113	112	rexrd 11247	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) ∈ ℝ*)
114		psmettri 24429	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
115	57, 60, 61, 82, 114	syl13anc 1395	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)))
116	93	simp3d 1160	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
117	77, 80, 91, 116	syl21anc 850	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118	107	simp3d 1160	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
119	77, 80, 105, 118	syl21anc 850	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
120	95, 109, 78, 117, 119	lt2halvesd 12483	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121	110, 120	eqbrtrd 5127	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +𝑒 (𝑟𝐷𝑞)) < 𝑎)
122	76, 113, 69, 115, 121	xrlelttrd 13176	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
123	74, 122	eqbrtrrid 5141	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
124	67, 69, 71, 75, 123	elicod 13413	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125		fvimacnv 7038	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (◡𝐷 “ (0[,)𝑎))))
126	125	biimpa 481	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (◡𝐷 “ (0[,)𝑎)))
127		df-br 5106	. . . . . . . . . . . . 13 ⊢ (𝑝(◡𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (◡𝐷 “ (0[,)𝑎)))
128	126, 127	sylibr 237	. . . . . . . . . . . 12 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)
129	59, 65, 124, 128	syl21anc 850	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ+) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)
130	51, 52, 53, 54, 129	syl22anc 851	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(◡𝐷 “ (0[,)𝑎))𝑞)
131	45	simprd 500	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (◡𝐷 “ (0[,)𝑎)))
132	131	breqd 5116	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞 ↔ 𝑝(◡𝐷 “ (0[,)𝑎))𝑞))
133	130, 132	mpbird 260	. . . . . . . . 9 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞)
134		df-br 5106	. . . . . . . . . . . . 13 ⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
135	134	bilanri 511	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞)
136		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑝 ∈ V
137		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
138	136, 137	brco 5847	. . . . . . . . . . . 12 ⊢ (𝑝((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
139	135, 138	sylib 221	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140	23	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
141	140, 25	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
142	31	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
143	141, 142	sseqtrd 3975	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
144	143	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145		vex 3461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑟 ∈ V
146	136, 145	brelrn 5923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2))))
147	146	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (◡𝐷 “ (0[,)(𝑎 / 2))))
148	144, 147	sseldd 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋)
149	148	adantrr 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
150	149	ex 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋))
151	150	ancrd 560	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
152	151	eximdv 1940	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
153	152	ad3antrrr 742	. . . . . . . . . . . . 13 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
154	153	3ad2ant1 1149	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
155	154	adantr 485	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → (∃𝑟(𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156	139, 155	mpd 16	. . . . . . . . . 10 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
157		df-rex 3090	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
158	156, 157	sylibr 237	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
159	133, 158	r19.29a 3173	. . . . . . . 8 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
160		df-br 5106	. . . . . . . 8 ⊢ (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
161	159, 160	sylib 221	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162	40, 41, 42, 43, 161	syl31anc 1396	. . . . . 6 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
163	39, 162	mpdan 699	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
164	163	ex 417	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
165	19, 164	relssdv 5765	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
166		id 23	. . . . . 6 ⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))))
167	166, 166	coeq12d 5841	. . . . 5 ⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))))
168	167	sseq1d 3970	. . . 4 ⊢ (𝑣 = (◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
169	168	rspcev 3584	. . 3 ⊢ (((◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
170	17, 165, 169	syl2anc 595	. 2 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ+) ∧ 𝐴 = (◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
171	9	metustel 24668	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
172	171	adantl 486	. . 3 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎))))
173	172	biimpa 481	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ+ 𝐴 = (◡𝐷 “ (0[,)𝑎)))
174	170, 173	r19.29a 3173	1 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ≠ wne 2960  ∃wrex 3089   ⊆ wss 3907  ∅c0 4288  ⟨cop 4591   class class class wbr 5105   ↦ cmpt 5186   × cxp 5650  ^◡ccnv 5651  dom cdm 5652  ran crn 5653   “ cima 5655   ∘ ccom 5656  Rel wrel 5657  Fun wfun 6519  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400  ℝcr 11087  0cc0 11088   + caddc 11091  ℝ^*cxr 11230   < clt 11231   ≤ cle 11232   / cdiv 11859  2c2 12286  ℝ⁺crp 13007   +_𝑒 cxad 13126  [,)cico 13365  PsMetcpsmet 21466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-map 8814  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12225  df-2 12294  df-rp 13008  df-xneg 13128  df-xadd 13129  df-xmul 13130  df-ico 13369  df-psmet 21474

This theorem is referenced by:  metust  24676