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 23166

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 782	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → 𝐷 ∈ (PsMet‘𝑋))
2		simplr 767	. . . . . 6 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → 𝑎 ∈ ℝ⁺)
3	2	rphalfcld 12444	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ⁺)
4		eqidd 2822	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)(𝑎 / 2))))
5		oveq2 7164	. . . . . . 7 ⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
6	5	imaeq2d 5929	. . . . . 6 ⊢ (𝑏 = (𝑎 / 2) → (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)(𝑎 / 2))))
7	6	rspceeqv 3638	. . . . 5 ⊢ (((𝑎 / 2) ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏)))
8	3, 4, 7	syl2anc 586	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏)))
9		metust.1	. . . . . . 7 ⊢ 𝐹 = ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
10		oveq2 7164	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
11	10	imaeq2d 5929	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)𝑏)))
12	11	cbvmptv 5169	. . . . . . . 8 ⊢ (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
13	12	rneqi 5807	. . . . . . 7 ⊢ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
14	9, 13	eqtri 2844	. . . . . 6 ⊢ 𝐹 = ran (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
15	14	metustel 23160	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏))))
16	15	biimpar 480	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
17	1, 8, 16	syl2anc 586	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18		relco 6097	. . . . 5 ⊢ Rel ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))
19	18	a1i 11	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → Rel ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
20		cossxp 6123	. . . . . . . . . 10 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
21		cnvimass 5949	. . . . . . . . . . . . . 14 ⊢ (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22		psmetf 22916	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
23	21, 22	fssdm 6530	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24		dmss 5771	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25		rnss 5809	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26		xpss12 5570	. . . . . . . . . . . . . 14 ⊢ ((dom (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
27	24, 25, 26	syl2anc 586	. . . . . . . . . . . . 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 484	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30		dmxp 5799	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31		rnxp 6027	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
32	30, 31	xpeq12d 5586	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
33	32	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
34	29, 33	sseqtrd 4007	. . . . . . . . . 10 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
35	20, 34	sstrid 3978	. . . . . . . . 9 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
36	35	ad3antrrr 728	. . . . . . . 8 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
37	36	sselda 3967	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38		opelxp 5591	. . . . . . 7 ⊢ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
39	37, 38	sylib 220	. . . . . 6 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
40		simpll 765	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
41		simprl 769	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑝 ∈ 𝑋)
42		simprr 771	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → 𝑞 ∈ 𝑋)
43		simplr 767	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
44		simplll 773	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
45	44	simp1d 1138	. . . . . . . . . . . . . 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 514	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺))
49	44	simp2d 1139	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
50	44	simp3d 1140	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
51	48, 49, 50	3jca 1124	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
52		simplr 767	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
53		simprl 769	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
54		simprr 771	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
55		simpll 765	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
56	55	simp1d 1138	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺))
57	56	simpld 497	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
58	22	ffund 6518	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
59	57, 58	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
60	55	simp2d 1139	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
61	55	simp3d 1140	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
62	60, 61	opelxpd 5593	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
63	22	fdmd 6523	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
64	57, 63	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
65	62, 64	eleqtrrd 2916	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66		0xr 10688	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ^*)
68	56	simprd 498	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ⁺)
69	68	rpxrd 12433	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ^*)
70	57, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
71	70, 62	ffvelrnd 6852	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ^*)
72		psmetge0 22922	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞))
73	57, 60, 61, 72	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74		df-ov 7159	. . . . . . . . . . . . . 14 ⊢ (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
75	73, 74	breqtrdi 5107	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
76	74, 71	eqeltrid 2917	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ^*)
77		0red 10644	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
78	68	rpred 12432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
79	78	rehalfcld 11885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
80	79	rexrd 10691	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ^*)
81		df-ov 7159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82		simplr 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
83	60, 82	opelxpd 5593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
84	83, 64	eleqtrrd 2916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86		df-br 5067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
87	85, 86	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
88		fvimacnv 6823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
89	88	biimpar 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
90	59, 84, 87, 89	syl21anc 835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
91	81, 90	eqeltrid 2917	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92		elico2 12801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
93	92	biimpa 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
94	93	simp1d 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
95	77, 80, 91, 94	syl21anc 835	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96		df-ov 7159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
97	82, 61	opelxpd 5593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
98	97, 64	eleqtrrd 2916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100		df-br 5067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
101	99, 100	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
102		fvimacnv 6823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
103	102	biimpar 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
104	59, 98, 101, 103	syl21anc 835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
105	96, 104	eqeltrid 2917	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106		elico2 12801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107	106	biimpa 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108	107	simp1d 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
109	77, 80, 105, 108	syl21anc 835	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
110	95, 109	rexaddd 12628	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
111	95, 109	readdcld 10670	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112	110, 111	eqeltrd 2913	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113	112	rexrd 10691	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) ∈ ℝ^*)
114		psmettri 22921	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)))
115	57, 60, 61, 82, 114	syl13anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)))
116	93	simp3d 1140	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
117	77, 80, 91, 116	syl21anc 835	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118	107	simp3d 1140	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
119	77, 80, 105, 118	syl21anc 835	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
120	95, 109, 78, 117, 119	lt2halvesd 11886	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121	110, 120	eqbrtrd 5088	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) < 𝑎)
122	76, 113, 69, 115, 121	xrlelttrd 12554	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
123	74, 122	eqbrtrrid 5102	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
124	67, 69, 71, 75, 123	elicod 12788	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125		fvimacnv 6823	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎))))
126	125	biimpa 479	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎)))
127		df-br 5067	. . . . . . . . . . . . 13 ⊢ (𝑝(^◡𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎)))
128	126, 127	sylibr 236	. . . . . . . . . . . 12 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞)
129	59, 65, 124, 128	syl21anc 835	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞)
130	51, 52, 53, 54, 129	syl22anc 836	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞)
131	45	simprd 498	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (^◡𝐷 “ (0[,)𝑎)))
132	131	breqd 5077	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞 ↔ 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞))
133	130, 132	mpbird 259	. . . . . . . . 9 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞)
134		simpr 487	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
135		df-br 5067	. . . . . . . . . . . . 13 ⊢ (𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
136	134, 135	sylibr 236	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞)
137		vex 3497	. . . . . . . . . . . . 13 ⊢ 𝑝 ∈ V
138		vex 3497	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
139	137, 138	brco 5741	. . . . . . . . . . . 12 ⊢ (𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140	136, 139	sylib 220	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
141	23	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
142	141, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
143	31	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
144	142, 143	sseqtrd 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145	144	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
146		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑟 ∈ V
147	137, 146	brelrn 5812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
148	147	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
149	145, 148	sseldd 3968	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋)
150	149	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
151	150	ex 415	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋))
152	151	ancrd 554	. . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . 13 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
155	154	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156	155	adantr 483	. . . . . . . . . . 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 3144	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑋 (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
159	157, 158	sylibr 236	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
160	133, 159	r19.29a 3289	. . . . . . . 8 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
161		df-br 5067	. . . . . . . 8 ⊢ (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162	160, 161	sylib 220	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
163	40, 41, 42, 43, 162	syl31anc 1369	. . . . . 6 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
164	39, 163	mpdan 685	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
165	164	ex 415	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
166	19, 165	relssdv 5661	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
167		id 22	. . . . . 6 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))))
168	167, 167	coeq12d 5735	. . . . 5 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
169	168	sseq1d 3998	. . . 4 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
170	169	rspcev 3623	. . 3 ⊢ (((^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
171	17, 166, 170	syl2anc 586	. 2 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
172	9	metustel 23160	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
173	172	adantl 484	. . 3 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
174	173	biimpa 479	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎)))
175	171, 174	r19.29a 3289	1 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∃wex 1780 ∈ wcel 2114 ≠ wne 3016 ∃wrex 3139 ⊆ wss 3936 ∅c0 4291 ⟨cop 4573 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 ^◡ccnv 5554 dom cdm 5555 ran crn 5556 “ cima 5558 ∘ ccom 5559 Rel wrel 5560 Fun wfun 6349 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ℝcr 10536 0cc0 10537 + caddc 10540 ℝ^*cxr 10674 < clt 10675 ≤ cle 10676 / cdiv 11297 2c2 11693 ℝ⁺crp 12390 +_𝑒 cxad 12506 [,)cico 12741 PsMetcpsmet 20529

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-po 5474 df-so 5475 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-1st 7689 df-2nd 7690 df-er 8289 df-map 8408 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-2 11701 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ico 12745 df-psmet 20537

This theorem is referenced by: metust 23168

W3C validator