Metamath Proof Explorer


Theorem 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 ffvelrnd ( ( ( ( ( 𝐷 ∈ ( 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 ‘ 𝑋 ) ) ∧ 𝐴𝐹 ) → ∃ 𝑣𝐹 ( 𝑣𝑣 ) ⊆ 𝐴 )