metustexhalf

Description: For any element A of the filter base generated by the metric D , 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)

		Ref	Expression
	Hypothesis	metust.1	⊢ 𝐹 = ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
	Assertion	metustexhalf	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) → ∃ 𝑣 ∈ 𝐹 ( 𝑣 ∘ 𝑣 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		metust.1	⊢ 𝐹 = ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2		simp-4r	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
3		simplr	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝑎 ∈ ℝ⁺ )
4	3	rphalfcld	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( 𝑎 / 2 ) ∈ ℝ⁺ )
5		eqidd	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
6		oveq2	⊢ ( 𝑏 = ( 𝑎 / 2 ) → ( 0 [,) 𝑏 ) = ( 0 [,) ( 𝑎 / 2 ) ) )
7	6	imaeq2d	⊢ ( 𝑏 = ( 𝑎 / 2 ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
8	7	rspceeqv	⊢ ( ( ( 𝑎 / 2 ) ∈ ℝ⁺ ∧ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) → ∃ 𝑏 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
9	4 5 8	syl2anc	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ∃ 𝑏 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
10		oveq2	⊢ ( 𝑎 = 𝑏 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑏 ) )
11	10	imaeq2d	⊢ ( 𝑎 = 𝑏 → ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
12	11	cbvmptv	⊢ ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
13	12	rneqi	⊢ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
14	1 13	eqtri	⊢ 𝐹 = ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) )
15	14	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∈ 𝐹 ↔ ∃ 𝑏 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) )
16	15	biimpar	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ∃ 𝑏 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∈ 𝐹 )
17	2 9 16	syl2anc	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∈ 𝐹 )
18		relco	⊢ Rel ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
19	18	a1i	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → Rel ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
20		cossxp	⊢ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) × ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
21		cnvimass	⊢ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ dom 𝐷
22		psmetf	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
23	21 22	fssdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ( 𝑋 × 𝑋 ) )
24		dmss	⊢ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ( 𝑋 × 𝑋 ) → dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ dom ( 𝑋 × 𝑋 ) )
25		rnss	⊢ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ( 𝑋 × 𝑋 ) → ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ran ( 𝑋 × 𝑋 ) )
26		xpss12	⊢ ( ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ dom ( 𝑋 × 𝑋 ) ∧ ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ran ( 𝑋 × 𝑋 ) ) → ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) × ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( dom ( 𝑋 × 𝑋 ) × ran ( 𝑋 × 𝑋 ) ) )
27	24 25 26	syl2anc	⊢ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ( 𝑋 × 𝑋 ) → ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) × ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( dom ( 𝑋 × 𝑋 ) × ran ( 𝑋 × 𝑋 ) ) )
28	23 27	syl	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) × ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( dom ( 𝑋 × 𝑋 ) × ran ( 𝑋 × 𝑋 ) ) )
29	28	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) × ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( dom ( 𝑋 × 𝑋 ) × ran ( 𝑋 × 𝑋 ) ) )
30		dmxp	⊢ ( 𝑋 ≠ ∅ → dom ( 𝑋 × 𝑋 ) = 𝑋 )
31		rnxp	⊢ ( 𝑋 ≠ ∅ → ran ( 𝑋 × 𝑋 ) = 𝑋 )
32	30 31	xpeq12d	⊢ ( 𝑋 ≠ ∅ → ( dom ( 𝑋 × 𝑋 ) × ran ( 𝑋 × 𝑋 ) ) = ( 𝑋 × 𝑋 ) )
33	32	adantr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( dom ( 𝑋 × 𝑋 ) × ran ( 𝑋 × 𝑋 ) ) = ( 𝑋 × 𝑋 ) )
34	29 33	sseqtrd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( dom ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) × ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( 𝑋 × 𝑋 ) )
35	20 34	sstrid	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( 𝑋 × 𝑋 ) )
36	35	ad3antrrr	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ ( 𝑋 × 𝑋 ) )
37	36	sselda	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) )
38		opelxp	⊢ ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) )
39	37 38	sylib	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) )
40		simpll	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
41		simprl	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → 𝑝 ∈ 𝑋 )
42		simprr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → 𝑞 ∈ 𝑋 )
43		simplr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
44		simplll	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) )
45	44	simp1d	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
46	45 2	syl	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
47	45 3	syl	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑎 ∈ ℝ⁺ )
48	46 47	jca	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) )
49	44	simp2d	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 ∈ 𝑋 )
50	44	simp3d	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑞 ∈ 𝑋 )
51	48 49 50	3jca	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) )
52		simplr	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑟 ∈ 𝑋 )
53		simprl	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 )
54		simprr	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 )
55		simpll	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) )
56	55	simp1d	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) )
57	56	simpld	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
58	22	ffund	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → Fun 𝐷 )
59	57 58	syl	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → Fun 𝐷 )
60	55	simp2d	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 ∈ 𝑋 )
61	55	simp3d	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑞 ∈ 𝑋 )
62	60 61	opelxpd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) )
63	22	fdmd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
64	57 63	syl	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
65	62 64	eleqtrrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 )
66		0xr	⊢ 0 ∈ ℝ^*
67	66	a1i	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 0 ∈ ℝ^* )
68	56	simprd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑎 ∈ ℝ⁺ )
69	68	rpxrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑎 ∈ ℝ^* )
70	57 22	syl	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
71	70 62	ffvelcdmd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ℝ^* )
72		psmetge0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → 0 ≤ ( 𝑝 𝐷 𝑞 ) )
73	57 60 61 72	syl3anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 0 ≤ ( 𝑝 𝐷 𝑞 ) )
74		df-ov	⊢ ( 𝑝 𝐷 𝑞 ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ )
75	73 74	breqtrdi	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 0 ≤ ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
76	74 71	eqeltrid	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐷 𝑞 ) ∈ ℝ^* )
77		0red	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 0 ∈ ℝ )
78	68	rpred	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑎 ∈ ℝ )
79	78	rehalfcld	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑎 / 2 ) ∈ ℝ )
80	79	rexrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑎 / 2 ) ∈ ℝ^* )
81		df-ov	⊢ ( 𝑝 𝐷 𝑟 ) = ( 𝐷 ‘ ⟨ 𝑝 , 𝑟 ⟩ )
82		simplr	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑟 ∈ 𝑋 )
83	60 82	opelxpd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑝 , 𝑟 ⟩ ∈ ( 𝑋 × 𝑋 ) )
84	83 64	eleqtrrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑝 , 𝑟 ⟩ ∈ dom 𝐷 )
85		simprl	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 )
86		df-br	⊢ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ↔ ⟨ 𝑝 , 𝑟 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
87	85 86	sylib	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑝 , 𝑟 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
88		fvimacnv	⊢ ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑟 ⟩ ∈ dom 𝐷 ) → ( ( 𝐷 ‘ ⟨ 𝑝 , 𝑟 ⟩ ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ↔ ⟨ 𝑝 , 𝑟 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
89	88	biimpar	⊢ ( ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑟 ⟩ ∈ dom 𝐷 ) ∧ ⟨ 𝑝 , 𝑟 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑟 ⟩ ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) )
90	59 84 87 89	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑟 ⟩ ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) )
91	81 90	eqeltrid	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐷 𝑟 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) )
92		elico2	⊢ ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) → ( ( 𝑝 𝐷 𝑟 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ↔ ( ( 𝑝 𝐷 𝑟 ) ∈ ℝ ∧ 0 ≤ ( 𝑝 𝐷 𝑟 ) ∧ ( 𝑝 𝐷 𝑟 ) < ( 𝑎 / 2 ) ) ) )
93	92	biimpa	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) ∧ ( 𝑝 𝐷 𝑟 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( ( 𝑝 𝐷 𝑟 ) ∈ ℝ ∧ 0 ≤ ( 𝑝 𝐷 𝑟 ) ∧ ( 𝑝 𝐷 𝑟 ) < ( 𝑎 / 2 ) ) )
94	93	simp1d	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) ∧ ( 𝑝 𝐷 𝑟 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( 𝑝 𝐷 𝑟 ) ∈ ℝ )
95	77 80 91 94	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐷 𝑟 ) ∈ ℝ )
96		df-ov	⊢ ( 𝑟 𝐷 𝑞 ) = ( 𝐷 ‘ ⟨ 𝑟 , 𝑞 ⟩ )
97	82 61	opelxpd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑟 , 𝑞 ⟩ ∈ ( 𝑋 × 𝑋 ) )
98	97 64	eleqtrrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑟 , 𝑞 ⟩ ∈ dom 𝐷 )
99		simprr	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 )
100		df-br	⊢ ( 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ↔ ⟨ 𝑟 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
101	99 100	sylib	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ⟨ 𝑟 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
102		fvimacnv	⊢ ( ( Fun 𝐷 ∧ ⟨ 𝑟 , 𝑞 ⟩ ∈ dom 𝐷 ) → ( ( 𝐷 ‘ ⟨ 𝑟 , 𝑞 ⟩ ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ↔ ⟨ 𝑟 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
103	102	biimpar	⊢ ( ( ( Fun 𝐷 ∧ ⟨ 𝑟 , 𝑞 ⟩ ∈ dom 𝐷 ) ∧ ⟨ 𝑟 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) → ( 𝐷 ‘ ⟨ 𝑟 , 𝑞 ⟩ ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) )
104	59 98 101 103	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ‘ ⟨ 𝑟 , 𝑞 ⟩ ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) )
105	96 104	eqeltrid	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑟 𝐷 𝑞 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) )
106		elico2	⊢ ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) → ( ( 𝑟 𝐷 𝑞 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ↔ ( ( 𝑟 𝐷 𝑞 ) ∈ ℝ ∧ 0 ≤ ( 𝑟 𝐷 𝑞 ) ∧ ( 𝑟 𝐷 𝑞 ) < ( 𝑎 / 2 ) ) ) )
107	106	biimpa	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) ∧ ( 𝑟 𝐷 𝑞 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( ( 𝑟 𝐷 𝑞 ) ∈ ℝ ∧ 0 ≤ ( 𝑟 𝐷 𝑞 ) ∧ ( 𝑟 𝐷 𝑞 ) < ( 𝑎 / 2 ) ) )
108	107	simp1d	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) ∧ ( 𝑟 𝐷 𝑞 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( 𝑟 𝐷 𝑞 ) ∈ ℝ )
109	77 80 105 108	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑟 𝐷 𝑞 ) ∈ ℝ )
110	95 109	rexaddd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝑝 𝐷 𝑟 ) +_𝑒 ( 𝑟 𝐷 𝑞 ) ) = ( ( 𝑝 𝐷 𝑟 ) + ( 𝑟 𝐷 𝑞 ) ) )
111	95 109	readdcld	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝑝 𝐷 𝑟 ) + ( 𝑟 𝐷 𝑞 ) ) ∈ ℝ )
112	110 111	eqeltrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝑝 𝐷 𝑟 ) +_𝑒 ( 𝑟 𝐷 𝑞 ) ) ∈ ℝ )
113	112	rexrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝑝 𝐷 𝑟 ) +_𝑒 ( 𝑟 𝐷 𝑞 ) ) ∈ ℝ^* )
114		psmettri	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) → ( 𝑝 𝐷 𝑞 ) ≤ ( ( 𝑝 𝐷 𝑟 ) +_𝑒 ( 𝑟 𝐷 𝑞 ) ) )
115	57 60 61 82 114	syl13anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐷 𝑞 ) ≤ ( ( 𝑝 𝐷 𝑟 ) +_𝑒 ( 𝑟 𝐷 𝑞 ) ) )
116	93	simp3d	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) ∧ ( 𝑝 𝐷 𝑟 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( 𝑝 𝐷 𝑟 ) < ( 𝑎 / 2 ) )
117	77 80 91 116	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐷 𝑟 ) < ( 𝑎 / 2 ) )
118	107	simp3d	⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝑎 / 2 ) ∈ ℝ^* ) ∧ ( 𝑟 𝐷 𝑞 ) ∈ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( 𝑟 𝐷 𝑞 ) < ( 𝑎 / 2 ) )
119	77 80 105 118	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑟 𝐷 𝑞 ) < ( 𝑎 / 2 ) )
120	95 109 78 117 119	lt2halvesd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝑝 𝐷 𝑟 ) + ( 𝑟 𝐷 𝑞 ) ) < 𝑎 )
121	110 120	eqbrtrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( ( 𝑝 𝐷 𝑟 ) +_𝑒 ( 𝑟 𝐷 𝑞 ) ) < 𝑎 )
122	76 113 69 115 121	xrlelttrd	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐷 𝑞 ) < 𝑎 )
123	74 122	eqbrtrrid	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) < 𝑎 )
124	67 69 71 75 123	elicod	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) )
125		fvimacnv	⊢ ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 ) → ( ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
126	125	biimpa	⊢ ( ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 ) ∧ ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
127		df-br	⊢ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) 𝑞 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
128	126 127	sylibr	⊢ ( ( ( Fun 𝐷 ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ dom 𝐷 ) ∧ ( 𝐷 ‘ ⟨ 𝑝 , 𝑞 ⟩ ) ∈ ( 0 [,) 𝑎 ) ) → 𝑝 ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) 𝑞 )
129	59 65 124 128	syl21anc	⊢ ( ( ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) 𝑞 )
130	51 52 53 54 129	syl22anc	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) 𝑞 )
131	45	simprd	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
132	131	breqd	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → ( 𝑝 𝐴 𝑞 ↔ 𝑝 ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) 𝑞 ) )
133	130 132	mpbird	⊢ ( ( ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ 𝑟 ∈ 𝑋 ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑝 𝐴 𝑞 )
134		simpr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
135		df-br	⊢ ( 𝑝 ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) 𝑞 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
136	134 135	sylibr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → 𝑝 ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) 𝑞 )
137		vex	⊢ 𝑝 ∈ V
138		vex	⊢ 𝑞 ∈ V
139	137 138	brco	⊢ ( 𝑝 ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) 𝑞 ↔ ∃ 𝑟 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) )
140	136 139	sylib	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ∃ 𝑟 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) )
141	23	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ( 𝑋 × 𝑋 ) )
142	141 25	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ ran ( 𝑋 × 𝑋 ) )
143	31	adantr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑋 × 𝑋 ) = 𝑋 )
144	142 143	sseqtrd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ 𝑋 )
145	144	adantr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ) → ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ⊆ 𝑋 )
146		vex	⊢ 𝑟 ∈ V
147	137 146	brelrn	⊢ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 → 𝑟 ∈ ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
148	147	adantl	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ) → 𝑟 ∈ ran ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
149	145 148	sseldd	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ) → 𝑟 ∈ 𝑋 )
150	149	adantrr	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) → 𝑟 ∈ 𝑋 )
151	150	ex	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) → 𝑟 ∈ 𝑋 ) )
152	151	ancrd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) → ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) ) )
153	152	eximdv	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ∃ 𝑟 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) → ∃ 𝑟 ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) ) )
154	153	ad3antrrr	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ∃ 𝑟 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) → ∃ 𝑟 ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) ) )
155	154	3ad2ant1	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( ∃ 𝑟 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) → ∃ 𝑟 ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) ) )
156	155	adantr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ( ∃ 𝑟 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) → ∃ 𝑟 ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) ) )
157	140 156	mpd	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ∃ 𝑟 ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) )
158		df-rex	⊢ ( ∃ 𝑟 ∈ 𝑋 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ↔ ∃ 𝑟 ( 𝑟 ∈ 𝑋 ∧ ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) ) )
159	157 158	sylibr	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ∃ 𝑟 ∈ 𝑋 ( 𝑝 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑟 ∧ 𝑟 ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) 𝑞 ) )
160	133 159	r19.29a	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → 𝑝 𝐴 𝑞 )
161		df-br	⊢ ( 𝑝 𝐴 𝑞 ↔ ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
162	160 161	sylib	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
163	40 41 42 43 162	syl31anc	⊢ ( ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
164	39 163	mpdan	⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∧ ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 )
165	164	ex	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ⟨ 𝑝 , 𝑞 ⟩ ∈ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) → ⟨ 𝑝 , 𝑞 ⟩ ∈ 𝐴 ) )
166	19 165	relssdv	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ 𝐴 )
167		id	⊢ ( 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) → 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) )
168	167 167	coeq12d	⊢ ( 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( 𝑣 ∘ 𝑣 ) = ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) )
169	168	sseq1d	⊢ ( 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) → ( ( 𝑣 ∘ 𝑣 ) ⊆ 𝐴 ↔ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ 𝐴 ) )
170	169	rspcev	⊢ ( ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∈ 𝐹 ∧ ( ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ∘ ( ^◡ 𝐷 “ ( 0 [,) ( 𝑎 / 2 ) ) ) ) ⊆ 𝐴 ) → ∃ 𝑣 ∈ 𝐹 ( 𝑣 ∘ 𝑣 ) ⊆ 𝐴 )
171	17 166 170	syl2anc	⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) ∧ 𝑎 ∈ ℝ⁺ ) ∧ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → ∃ 𝑣 ∈ 𝐹 ( 𝑣 ∘ 𝑣 ) ⊆ 𝐴 )
172	1	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ⁺ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
173	172	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ⁺ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
174	173	biimpa	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) → ∃ 𝑎 ∈ ℝ⁺ 𝐴 = ( ^◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
175	171 174	r19.29a	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝐹 ) → ∃ 𝑣 ∈ 𝐹 ( 𝑣 ∘ 𝑣 ) ⊆ 𝐴 )

Metamath Proof Explorer

Theorem metustexhalf

Proof