metustexhalf - Metamath Proof Explorer

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

Theorem metustexhalf 23322

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 784	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2		simplr 769	. . . . . 6 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ⁺)
3	2	rphalfcld 12539	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ⁺)
4		eqidd 2740	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)(𝑎 / 2))))
5		oveq2 7191	. . . . . . 7 ⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
6	5	imaeq2d 5913	. . . . . 6 ⊢ (𝑏 = (𝑎 / 2) → (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)(𝑎 / 2))))
7	6	rspceeqv 3544	. . . . 5 ⊢ (((𝑎 / 2) ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏)))
8	3, 4, 7	syl2anc 587	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏)))
9		metust.1	. . . . . . 7 ⊢ 𝐹 = ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
10		oveq2 7191	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
11	10	imaeq2d 5913	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)𝑏)))
12	11	cbvmptv 5143	. . . . . . . 8 ⊢ (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
13	12	rneqi 5790	. . . . . . 7 ⊢ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
14	9, 13	eqtri 2762	. . . . . 6 ⊢ 𝐹 = ran (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
15	14	metustel 23316	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏))))
16	15	biimpar 481	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
17	1, 8, 16	syl2anc 587	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18		relco 6087	. . . . 5 ⊢ Rel ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))
19	18	a1i 11	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → Rel ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
20		cossxp 6114	. . . . . . . . . 10 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
21		cnvimass 5933	. . . . . . . . . . . . . 14 ⊢ (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22		psmetf 23072	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
23	21, 22	fssdm 6535	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24		dmss 5755	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25		rnss 5792	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26		xpss12 5550	. . . . . . . . . . . . . 14 ⊢ ((dom (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
27	24, 25, 26	syl2anc 587	. . . . . . . . . . . . 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 485	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30		dmxp 5782	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31		rnxp 6012	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
32	30, 31	xpeq12d 5566	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
33	32	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
34	29, 33	sseqtrd 3927	. . . . . . . . . 10 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
35	20, 34	sstrid 3898	. . . . . . . . 9 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
36	35	ad3antrrr 730	. . . . . . . 8 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
37	36	sselda 3887	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38		opelxp 5571	. . . . . . 7 ⊢ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
39	37, 38	sylib 221	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
40		simpll 767	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
41		simprl 771	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑝 ∈ 𝑋)
42		simprr 773	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑞 ∈ 𝑋)
43		simplr 769	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
44		simplll 775	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
45	44	simp1d 1143	. . . . . . . . . . . . . 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 515	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺))
49	44	simp2d 1144	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
50	44	simp3d 1145	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
51	48, 49, 50	3jca 1129	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
52		simplr 769	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
53		simprl 771	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
54		simprr 773	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
55		simpll 767	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
56	55	simp1d 1143	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺))
57	56	simpld 498	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
58	22	ffund 6519	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
59	57, 58	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
60	55	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
61	55	simp3d 1145	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
62	60, 61	opelxpd 5573	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
63	22	fdmd 6526	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
64	57, 63	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
65	62, 64	eleqtrrd 2837	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66		0xr 10779	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ^*)
68	56	simprd 499	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ⁺)
69	68	rpxrd 12528	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ^*)
70	57, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
71	70, 62	ffvelrnd 6875	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ^*)
72		psmetge0 23078	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞))
73	57, 60, 61, 72	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74		df-ov 7186	. . . . . . . . . . . . . 14 ⊢ (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
75	73, 74	breqtrdi 5081	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
76	74, 71	eqeltrid 2838	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ^*)
77		0red 10735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
78	68	rpred 12527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
79	78	rehalfcld 11976	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
80	79	rexrd 10782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ^*)
81		df-ov 7186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
83	60, 82	opelxpd 5573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
84	83, 64	eleqtrrd 2837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85		simprl 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86		df-br 5041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
87	85, 86	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
88		fvimacnv 6843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
89	88	biimpar 481	. . . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92		elico2 12898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
93	92	biimpa 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
94	93	simp1d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
95	77, 80, 91, 94	syl21anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96		df-ov 7186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
97	82, 61	opelxpd 5573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
98	97, 64	eleqtrrd 2837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99		simprr 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100		df-br 5041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
101	99, 100	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
102		fvimacnv 6843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
103	102	biimpar 481	. . . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106		elico2 12898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107	106	biimpa 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108	107	simp1d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
109	77, 80, 105, 108	syl21anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
110	95, 109	rexaddd 12723	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
111	95, 109	readdcld 10761	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112	110, 111	eqeltrd 2834	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113	112	rexrd 10782	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) ∈ ℝ^*)
114		psmettri 23077	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)))
115	57, 60, 61, 82, 114	syl13anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)))
116	93	simp3d 1145	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
117	77, 80, 91, 116	syl21anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118	107	simp3d 1145	. . . . . . . . . . . . . . . . . 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 11977	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121	110, 120	eqbrtrd 5062	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) < 𝑎)
122	76, 113, 69, 115, 121	xrlelttrd 12649	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
123	74, 122	eqbrtrrid 5076	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
124	67, 69, 71, 75, 123	elicod 12884	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125		fvimacnv 6843	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎))))
126	125	biimpa 480	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎)))
127		df-br 5041	. . . . . . . . . . . . 13 ⊢ (𝑝(^◡𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎)))
128	126, 127	sylibr 237	. . . . . . . . . . . 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 499	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (^◡𝐷 “ (0[,)𝑎)))
132	131	breqd 5051	. . . . . . . . . 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		simpr 488	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
135		df-br 5041	. . . . . . . . . . . . 13 ⊢ (𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
136	134, 135	sylibr 237	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞)
137		vex 3404	. . . . . . . . . . . . 13 ⊢ 𝑝 ∈ V
138		vex 3404	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
139	137, 138	brco 5723	. . . . . . . . . . . 12 ⊢ (𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140	136, 139	sylib 221	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
141	23	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
142	141, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
143	31	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
144	142, 143	sseqtrd 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145	144	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
146		vex 3404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑟 ∈ V
147	137, 146	brelrn 5795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
148	147	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
149	145, 148	sseldd 3888	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋)
150	149	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
151	150	ex 416	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋))
152	151	ancrd 555	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
153	152	eximdv 1924	. . . . . . . . . . . . . 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 1134	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156	155	adantr 484	. . . . . . . . . . 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 3060	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑋 (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
159	157, 158	sylibr 237	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
160	133, 159	r19.29a 3200	. . . . . . . 8 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
161		df-br 5041	. . . . . . . 8 ⊢ (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162	160, 161	sylib 221	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
163	40, 41, 42, 43, 162	syl31anc 1374	. . . . . 6 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
164	39, 163	mpdan 687	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
165	164	ex 416	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
166	19, 165	relssdv 5642	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
167		id 22	. . . . . 6 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))))
168	167, 167	coeq12d 5717	. . . . 5 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
169	168	sseq1d 3918	. . . 4 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
170	169	rspcev 3529	. . 3 ⊢ (((^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
171	17, 166, 170	syl2anc 587	. 2 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
172	9	metustel 23316	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
173	172	adantl 485	. . 3 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
174	173	biimpa 480	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎)))
175	171, 174	r19.29a 3200	1 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∃wex 1786 ∈ wcel 2114 ≠ wne 2935 ∃wrex 3055 ⊆ wss 3853 ∅c0 4221 ⟨cop 4532 class class class wbr 5040 ↦ cmpt 5120 × cxp 5533 ^◡ccnv 5534 dom cdm 5535 ran crn 5536 “ cima 5538 ∘ ccom 5539 Rel wrel 5540 Fun wfun 6344 ⟶wf 6346 ‘cfv 6350 (class class class)co 7183 ℝcr 10627 0cc0 10628 + caddc 10631 ℝ^*cxr 10765 < clt 10766 ≤ cle 10767 / cdiv 11388 2c2 11784 ℝ⁺crp 12485 +_𝑒 cxad 12601 [,)cico 12836 PsMetcpsmet 20214

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5177 ax-nul 5184 ax-pow 5242 ax-pr 5306 ax-un 7492 ax-cnex 10684 ax-resscn 10685 ax-1cn 10686 ax-icn 10687 ax-addcl 10688 ax-addrcl 10689 ax-mulcl 10690 ax-mulrcl 10691 ax-mulcom 10692 ax-addass 10693 ax-mulass 10694 ax-distr 10695 ax-i2m1 10696 ax-1ne0 10697 ax-1rid 10698 ax-rnegex 10699 ax-rrecex 10700 ax-cnre 10701 ax-pre-lttri 10702 ax-pre-lttrn 10703 ax-pre-ltadd 10704 ax-pre-mulgt0 10705

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3402 df-sbc 3686 df-csb 3801 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4807 df-iun 4893 df-br 5041 df-opab 5103 df-mpt 5121 df-id 5439 df-po 5452 df-so 5453 df-xp 5541 df-rel 5542 df-cnv 5543 df-co 5544 df-dm 5545 df-rn 5546 df-res 5547 df-ima 5548 df-iota 6308 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-riota 7140 df-ov 7186 df-oprab 7187 df-mpo 7188 df-1st 7727 df-2nd 7728 df-er 8333 df-map 8452 df-en 8569 df-dom 8570 df-sdom 8571 df-pnf 10768 df-mnf 10769 df-xr 10770 df-ltxr 10771 df-le 10772 df-sub 10963 df-neg 10964 df-div 11389 df-2 11792 df-rp 12486 df-xneg 12603 df-xadd 12604 df-xmul 12605 df-ico 12840 df-psmet 20222

This theorem is referenced by: metust 23324

W3C validator