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 24064

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 13027	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (𝑎 / 2) ∈ ℝ⁺)
4		eqidd 2733	. . . . 5 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)(𝑎 / 2))))
5		oveq2 7416	. . . . . . 7 ⊢ (𝑏 = (𝑎 / 2) → (0[,)𝑏) = (0[,)(𝑎 / 2)))
6	5	imaeq2d 6059	. . . . . 6 ⊢ (𝑏 = (𝑎 / 2) → (^◡𝐷 “ (0[,)𝑏)) = (^◡𝐷 “ (0[,)(𝑎 / 2))))
7	6	rspceeqv 3633	. . . . 5 ⊢ (((𝑎 / 2) ∈ ℝ⁺ ∧ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)(𝑎 / 2)))) → ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏)))
8	3, 4, 7	syl2anc 584	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏)))
9		metust.1	. . . . . . 7 ⊢ 𝐹 = ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎)))
10		oveq2 7416	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (0[,)𝑎) = (0[,)𝑏))
11	10	imaeq2d 6059	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (^◡𝐷 “ (0[,)𝑎)) = (^◡𝐷 “ (0[,)𝑏)))
12	11	cbvmptv 5261	. . . . . . . 8 ⊢ (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
13	12	rneqi 5936	. . . . . . 7 ⊢ ran (𝑎 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑎))) = ran (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
14	9, 13	eqtri 2760	. . . . . 6 ⊢ 𝐹 = ran (𝑏 ∈ ℝ⁺ ↦ (^◡𝐷 “ (0[,)𝑏)))
15	14	metustel 24058	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ↔ ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏))))
16	15	biimpar 478	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ ∃𝑏 ∈ ℝ⁺ (^◡𝐷 “ (0[,)(𝑎 / 2))) = (^◡𝐷 “ (0[,)𝑏))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
17	1, 8, 16	syl2anc 584	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹)
18		relco 6107	. . . . 5 ⊢ Rel ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))
19	18	a1i 11	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → Rel ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
20		cossxp 6271	. . . . . . . . . 10 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
21		cnvimass 6080	. . . . . . . . . . . . . 14 ⊢ (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom 𝐷
22		psmetf 23811	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
23	21, 22	fssdm 6737	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
24		dmss 5902	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → dom (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋))
25		rnss 5938	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
26		xpss12 5691	. . . . . . . . . . . . . 14 ⊢ ((dom (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ dom (𝑋 × 𝑋) ∧ ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
27	24, 25, 26	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
28	23, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
29	28	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)))
30		dmxp 5928	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → dom (𝑋 × 𝑋) = 𝑋)
31		rnxp 6169	. . . . . . . . . . . . 13 ⊢ (𝑋 ≠ ∅ → ran (𝑋 × 𝑋) = 𝑋)
32	30, 31	xpeq12d 5707	. . . . . . . . . . . 12 ⊢ (𝑋 ≠ ∅ → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
33	32	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (𝑋 × 𝑋) × ran (𝑋 × 𝑋)) = (𝑋 × 𝑋))
34	29, 33	sseqtrd 4022	. . . . . . . . . 10 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (dom (^◡𝐷 “ (0[,)(𝑎 / 2))) × ran (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
35	20, 34	sstrid 3993	. . . . . . . . 9 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
36	35	ad3antrrr 728	. . . . . . . 8 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ (𝑋 × 𝑋))
37	36	sselda 3982	. . . . . . 7 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
38		opelxp 5712	. . . . . . 7 ⊢ (⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋) ↔ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
39	37, 38	sylib 217	. . . . . 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 1142	. . . . . . . . . . . . . 14 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
46	45, 1	syl 17	. . . . . . . . . . . . 13 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
47	45, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ⁺)
48	46, 47	jca 512	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺))
49	44	simp2d 1143	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
50	44	simp3d 1144	. . . . . . . . . . . 12 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
51	48, 49, 50	3jca 1128	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋))
52		simplr 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 1142	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺))
57	56	simpld 495	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷 ∈ (PsMet‘𝑋))
58	22	ffund 6721	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (PsMet‘𝑋) → Fun 𝐷)
59	57, 58	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → Fun 𝐷)
60	55	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝 ∈ 𝑋)
61	55	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑞 ∈ 𝑋)
62	60, 61	opelxpd 5715	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ (𝑋 × 𝑋))
63	22	fdmd 6728	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (PsMet‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
64	57, 63	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → dom 𝐷 = (𝑋 × 𝑋))
65	62, 64	eleqtrrd 2836	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑞⟩ ∈ dom 𝐷)
66		0xr 11260	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ^*)
68	56	simprd 496	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ⁺)
69	68	rpxrd 13016	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ^*)
70	57, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
71	70, 62	ffvelcdmd 7087	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ ℝ^*)
72		psmetge0 23817	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → 0 ≤ (𝑝𝐷𝑞))
73	57, 60, 61, 72	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝑝𝐷𝑞))
74		df-ov 7411	. . . . . . . . . . . . . 14 ⊢ (𝑝𝐷𝑞) = (𝐷‘⟨𝑝, 𝑞⟩)
75	73, 74	breqtrdi 5189	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ≤ (𝐷‘⟨𝑝, 𝑞⟩))
76	74, 71	eqeltrid 2837	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ∈ ℝ^*)
77		0red 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 0 ∈ ℝ)
78	68	rpred 13015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑎 ∈ ℝ)
79	78	rehalfcld 12458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ)
80	79	rexrd 11263	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑎 / 2) ∈ ℝ^*)
81		df-ov 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝𝐷𝑟) = (𝐷‘⟨𝑝, 𝑟⟩)
82		simplr 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
83	60, 82	opelxpd 5715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (𝑋 × 𝑋))
84	83, 64	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ dom 𝐷)
85		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟)
86		df-br 5149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ↔ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
87	85, 86	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
88		fvimacnv 7054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
89	88	biimpar 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑟⟩ ∈ dom 𝐷) ∧ ⟨𝑝, 𝑟⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
90	59, 84, 87, 89	syl21anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑟⟩) ∈ (0[,)(𝑎 / 2)))
91	81, 90	eqeltrid 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)))
92		elico2 13387	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) → ((𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2))))
93	92	biimpa 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → ((𝑝𝐷𝑟) ∈ ℝ ∧ 0 ≤ (𝑝𝐷𝑟) ∧ (𝑝𝐷𝑟) < (𝑎 / 2)))
94	93	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) ∈ ℝ)
95	77, 80, 91, 94	syl21anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) ∈ ℝ)
96		df-ov 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟𝐷𝑞) = (𝐷‘⟨𝑟, 𝑞⟩)
97	82, 61	opelxpd 5715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (𝑋 × 𝑋))
98	97, 64	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ dom 𝐷)
99		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)
100		df-br 5149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞 ↔ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
101	99, 100	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2))))
102		fvimacnv 7054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)) ↔ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
103	102	biimpar 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun 𝐷 ∧ ⟨𝑟, 𝑞⟩ ∈ dom 𝐷) ∧ ⟨𝑟, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
104	59, 98, 101, 103	syl21anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑟, 𝑞⟩) ∈ (0[,)(𝑎 / 2)))
105	96, 104	eqeltrid 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)))
106		elico2 13387	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) → ((𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2)) ↔ ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2))))
107	106	biimpa 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → ((𝑟𝐷𝑞) ∈ ℝ ∧ 0 ≤ (𝑟𝐷𝑞) ∧ (𝑟𝐷𝑞) < (𝑎 / 2)))
108	107	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) ∈ ℝ)
109	77, 80, 105, 108	syl21anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) ∈ ℝ)
110	95, 109	rexaddd 13212	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) = ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)))
111	95, 109	readdcld 11242	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) ∈ ℝ)
112	110, 111	eqeltrd 2833	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) ∈ ℝ)
113	112	rexrd 11263	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) ∈ ℝ^*)
114		psmettri 23816	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)))
115	57, 60, 61, 82, 114	syl13anc 1372	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) ≤ ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)))
116	93	simp3d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑝𝐷𝑟) ∈ (0[,)(𝑎 / 2))) → (𝑝𝐷𝑟) < (𝑎 / 2))
117	77, 80, 91, 116	syl21anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑟) < (𝑎 / 2))
118	107	simp3d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℝ ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑟𝐷𝑞) ∈ (0[,)(𝑎 / 2))) → (𝑟𝐷𝑞) < (𝑎 / 2))
119	77, 80, 105, 118	syl21anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑟𝐷𝑞) < (𝑎 / 2))
120	95, 109, 78, 117, 119	lt2halvesd 12459	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) + (𝑟𝐷𝑞)) < 𝑎)
121	110, 120	eqbrtrd 5170	. . . . . . . . . . . . . . 15 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → ((𝑝𝐷𝑟) +_𝑒 (𝑟𝐷𝑞)) < 𝑎)
122	76, 113, 69, 115, 121	xrlelttrd 13138	. . . . . . . . . . . . . 14 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐷𝑞) < 𝑎)
123	74, 122	eqbrtrrid 5184	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) < 𝑎)
124	67, 69, 71, 75, 123	elicod 13373	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎))
125		fvimacnv 7054	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) → ((𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎) ↔ ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎))))
126	125	biimpa 477	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎)))
127		df-br 5149	. . . . . . . . . . . . 13 ⊢ (𝑝(^◡𝐷 “ (0[,)𝑎))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ (^◡𝐷 “ (0[,)𝑎)))
128	126, 127	sylibr 233	. . . . . . . . . . . 12 ⊢ (((Fun 𝐷 ∧ ⟨𝑝, 𝑞⟩ ∈ dom 𝐷) ∧ (𝐷‘⟨𝑝, 𝑞⟩) ∈ (0[,)𝑎)) → 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞)
129	59, 65, 124, 128	syl21anc 836	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞)
130	51, 52, 53, 54, 129	syl22anc 837	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞)
131	45	simprd 496	. . . . . . . . . . 11 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝐴 = (^◡𝐷 “ (0[,)𝑎)))
132	131	breqd 5159	. . . . . . . . . 10 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → (𝑝𝐴𝑞 ↔ 𝑝(^◡𝐷 “ (0[,)𝑎))𝑞))
133	130, 132	mpbird 256	. . . . . . . . 9 ⊢ (((((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ 𝑟 ∈ 𝑋) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑝𝐴𝑞)
134		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
135		df-br 5149	. . . . . . . . . . . . 13 ⊢ (𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
136	134, 135	sylibr 233	. . . . . . . . . . . 12 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞)
137		vex 3478	. . . . . . . . . . . . 13 ⊢ 𝑝 ∈ V
138		vex 3478	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
139	137, 138	brco 5870	. . . . . . . . . . . 12 ⊢ (𝑝((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))𝑞 ↔ ∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
140	136, 139	sylib 217	. . . . . . . . . . 11 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
141	23	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ (𝑋 × 𝑋))
142	141, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ ran (𝑋 × 𝑋))
143	31	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑋 × 𝑋) = 𝑋)
144	142, 143	sseqtrd 4022	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
145	144	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → ran (^◡𝐷 “ (0[,)(𝑎 / 2))) ⊆ 𝑋)
146		vex 3478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑟 ∈ V
147	137, 146	brelrn 5941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 → 𝑟 ∈ ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
148	147	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ ran (^◡𝐷 “ (0[,)(𝑎 / 2))))
149	145, 148	sseldd 3983	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟) → 𝑟 ∈ 𝑋)
150	149	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)) → 𝑟 ∈ 𝑋)
151	150	ex 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → 𝑟 ∈ 𝑋))
152	151	ancrd 552	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → (𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
153	152	eximdv 1920	. . . . . . . . . . . . . 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 1133	. . . . . . . . . . . 12 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) → (∃𝑟(𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) → ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))))
156	155	adantr 481	. . . . . . . . . . 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 3071	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ 𝑋 (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞) ↔ ∃𝑟(𝑟 ∈ 𝑋 ∧ (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞)))
159	157, 158	sylibr 233	. . . . . . . . 9 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ∃𝑟 ∈ 𝑋 (𝑝(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑟 ∧ 𝑟(^◡𝐷 “ (0[,)(𝑎 / 2)))𝑞))
160	133, 159	r19.29a 3162	. . . . . . . 8 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → 𝑝𝐴𝑞)
161		df-br 5149	. . . . . . . 8 ⊢ (𝑝𝐴𝑞 ↔ ⟨𝑝, 𝑞⟩ ∈ 𝐴)
162	160, 161	sylib 217	. . . . . . 7 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
163	40, 41, 42, 43, 162	syl31anc 1373	. . . . . 6 ⊢ (((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) ∧ (𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋)) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
164	39, 163	mpdan 685	. . . . 5 ⊢ ((((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) ∧ ⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2))))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴)
165	164	ex 413	. . . 4 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → (⟨𝑝, 𝑞⟩ ∈ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) → ⟨𝑝, 𝑞⟩ ∈ 𝐴))
166	19, 165	relssdv 5788	. . 3 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴)
167		id 22	. . . . . 6 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → 𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))))
168	167, 167	coeq12d 5864	. . . . 5 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → (𝑣 ∘ 𝑣) = ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))))
169	168	sseq1d 4013	. . . 4 ⊢ (𝑣 = (^◡𝐷 “ (0[,)(𝑎 / 2))) → ((𝑣 ∘ 𝑣) ⊆ 𝐴 ↔ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴))
170	169	rspcev 3612	. . 3 ⊢ (((^◡𝐷 “ (0[,)(𝑎 / 2))) ∈ 𝐹 ∧ ((^◡𝐷 “ (0[,)(𝑎 / 2))) ∘ (^◡𝐷 “ (0[,)(𝑎 / 2)))) ⊆ 𝐴) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
171	17, 166, 170	syl2anc 584	. 2 ⊢ (((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) ∧ 𝑎 ∈ ℝ⁺) ∧ 𝐴 = (^◡𝐷 “ (0[,)𝑎))) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
172	9	metustel 24058	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
173	172	adantl 482	. . 3 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐴 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎))))
174	173	biimpa 477	. 2 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑎 ∈ ℝ⁺ 𝐴 = (^◡𝐷 “ (0[,)𝑎)))
175	171, 174	r19.29a 3162	1 ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ≠ wne 2940 ∃wrex 3070 ⊆ wss 3948 ∅c0 4322 ⟨cop 4634 class class class wbr 5148 ↦ cmpt 5231 × cxp 5674 ^◡ccnv 5675 dom cdm 5676 ran crn 5677 “ cima 5679 ∘ ccom 5680 Rel wrel 5681 Fun wfun 6537 ⟶wf 6539 ‘cfv 6543 (class class class)co 7408 ℝcr 11108 0cc0 11109 + caddc 11112 ℝ^*cxr 11246 < clt 11247 ≤ cle 11248 / cdiv 11870 2c2 12266 ℝ⁺crp 12973 +_𝑒 cxad 13089 [,)cico 13325 PsMetcpsmet 20927

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7974 df-2nd 7975 df-er 8702 df-map 8821 df-en 8939 df-dom 8940 df-sdom 8941 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11445 df-neg 11446 df-div 11871 df-2 12274 df-rp 12974 df-xneg 13091 df-xadd 13092 df-xmul 13093 df-ico 13329 df-psmet 20935

This theorem is referenced by: metust 24066

W3C validator