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 
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metustexhalf 
|- ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ A e. F ) -> E. v e. F ( v o. v ) C_ A )

Proof

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