Metamath Proof Explorer

Theorem restmetu

Description: The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017)

Ref Expression
Assertion restmetu 
|- ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( ( metUnif ` D ) |`t ( A X. A ) ) = ( metUnif ` ( D |` ( A X. A ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> A =/= (/) )
2 psmetres2 
 |-  ( ( D e. ( PsMet ` X ) /\ A C_ X ) -> ( D |` ( A X. A ) ) e. ( PsMet ` A ) )
3 2 3adant1 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( D |` ( A X. A ) ) e. ( PsMet ` A ) )
4 oveq2 
 |-  ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
5 4 imaeq2d 
 |-  ( a = b -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
6 5 cbvmptv 
 |-  ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ( b e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
7 6 rneqi 
 |-  ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ran ( b e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
8 7 metustfbas 
 |-  ( ( A =/= (/) /\ ( D |` ( A X. A ) ) e. ( PsMet ` A ) ) -> ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) e. ( fBas ` ( A X. A ) ) )
9 1 3 8 syl2anc 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) e. ( fBas ` ( A X. A ) ) )
10 fgval 
 |-  ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) e. ( fBas ` ( A X. A ) ) -> ( ( A X. A ) filGen ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) ) = { v e. ~P ( A X. A ) | ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) } )
11 9 10 syl 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( ( A X. A ) filGen ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) ) = { v e. ~P ( A X. A ) | ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) } )
12 metuval 
 |-  ( ( D |` ( A X. A ) ) e. ( PsMet ` A ) -> ( metUnif ` ( D |` ( A X. A ) ) ) = ( ( A X. A ) filGen ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) ) )
13 3 12 syl 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( metUnif ` ( D |` ( A X. A ) ) ) = ( ( A X. A ) filGen ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) ) )
14 fvex 
 |-  ( metUnif ` D ) e. _V
15 3 elfvexd 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> A e. _V )
16 15 15 xpexd 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
17 restval 
 |-  ( ( ( metUnif ` D ) e. _V /\ ( A X. A ) e. _V ) -> ( ( metUnif ` D ) |`t ( A X. A ) ) = ran ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) )
18 14 16 17 sylancr 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( ( metUnif ` D ) |`t ( A X. A ) ) = ran ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) )
19 inss2 
 |-  ( v i^i ( A X. A ) ) C_ ( A X. A )
20 sseq1 
 |-  ( u = ( v i^i ( A X. A ) ) -> ( u C_ ( A X. A ) <-> ( v i^i ( A X. A ) ) C_ ( A X. A ) ) )
21 19 20 mpbiri 
 |-  ( u = ( v i^i ( A X. A ) ) -> u C_ ( A X. A ) )
22 vex 
 |-  u e. _V
23 22 elpw 
 |-  ( u e. ~P ( A X. A ) <-> u C_ ( A X. A ) )
24 21 23 sylibr 
 |-  ( u = ( v i^i ( A X. A ) ) -> u e. ~P ( A X. A ) )
25 24 rexlimivw 
 |-  ( E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) -> u e. ~P ( A X. A ) )
26 25 adantl 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) ) -> u e. ~P ( A X. A ) )
27 nfv 
 |-  F/ a ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) )
28 nfmpt1 
 |-  F/_ a ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
29 28 nfrn 
 |-  F/_ a ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
30 29 nfcri 
 |-  F/ a w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
31 27 30 nfan 
 |-  F/ a ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) )
32 nfv 
 |-  F/ a w C_ v
33 31 32 nfan 
 |-  F/ a ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v )
34 nfmpt1 
 |-  F/_ a ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
35 34 nfrn 
 |-  F/_ a ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
36 nfcv 
 |-  F/_ a ~P u
37 35 36 nfin 
 |-  F/_ a ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u )
38 nfcv 
 |-  F/_ a (/)
39 37 38 nfne 
 |-  F/ a ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/)
40 simplr 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> a e. RR+ )
41 ineq1 
 |-  ( w = ( `' D " ( 0 [,) a ) ) -> ( w i^i ( A X. A ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
42 41 adantl 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( w i^i ( A X. A ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
43 simp2 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> D e. ( PsMet ` X ) )
44 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
45 ffun 
 |-  ( D : ( X X. X ) --> RR* -> Fun D )
46 respreima 
 |-  ( Fun D -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
47 43 44 45 46 4syl 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
48 47 ad6antr 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
49 42 48 eqtr4d 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( w i^i ( A X. A ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
50 rspe 
 |-  ( ( a e. RR+ /\ ( w i^i ( A X. A ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) -> E. a e. RR+ ( w i^i ( A X. A ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
51 40 49 50 syl2anc 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> E. a e. RR+ ( w i^i ( A X. A ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
52 vex 
 |-  w e. _V
53 52 inex1 
 |-  ( w i^i ( A X. A ) ) e. _V
54 eqid 
 |-  ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
55 54 elrnmpt 
 |-  ( ( w i^i ( A X. A ) ) e. _V -> ( ( w i^i ( A X. A ) ) e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) <-> E. a e. RR+ ( w i^i ( A X. A ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) )
56 53 55 ax-mp 
 |-  ( ( w i^i ( A X. A ) ) e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) <-> E. a e. RR+ ( w i^i ( A X. A ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
57 51 56 sylibr 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( w i^i ( A X. A ) ) e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) )
58 simpllr 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> w C_ v )
59 ssinss1 
 |-  ( w C_ v -> ( w i^i ( A X. A ) ) C_ v )
60 58 59 syl 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( w i^i ( A X. A ) ) C_ v )
61 inss2 
 |-  ( w i^i ( A X. A ) ) C_ ( A X. A )
62 61 a1i 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( w i^i ( A X. A ) ) C_ ( A X. A ) )
63 pweq 
 |-  ( u = ( v i^i ( A X. A ) ) -> ~P u = ~P ( v i^i ( A X. A ) ) )
64 63 eleq2d 
 |-  ( u = ( v i^i ( A X. A ) ) -> ( ( w i^i ( A X. A ) ) e. ~P u <-> ( w i^i ( A X. A ) ) e. ~P ( v i^i ( A X. A ) ) ) )
65 53 elpw 
 |-  ( ( w i^i ( A X. A ) ) e. ~P ( v i^i ( A X. A ) ) <-> ( w i^i ( A X. A ) ) C_ ( v i^i ( A X. A ) ) )
66 64 65 bitrdi 
 |-  ( u = ( v i^i ( A X. A ) ) -> ( ( w i^i ( A X. A ) ) e. ~P u <-> ( w i^i ( A X. A ) ) C_ ( v i^i ( A X. A ) ) ) )
67 ssin 
 |-  ( ( ( w i^i ( A X. A ) ) C_ v /\ ( w i^i ( A X. A ) ) C_ ( A X. A ) ) <-> ( w i^i ( A X. A ) ) C_ ( v i^i ( A X. A ) ) )
68 66 67 bitr4di 
 |-  ( u = ( v i^i ( A X. A ) ) -> ( ( w i^i ( A X. A ) ) e. ~P u <-> ( ( w i^i ( A X. A ) ) C_ v /\ ( w i^i ( A X. A ) ) C_ ( A X. A ) ) ) )
69 68 ad5antlr 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( ( w i^i ( A X. A ) ) e. ~P u <-> ( ( w i^i ( A X. A ) ) C_ v /\ ( w i^i ( A X. A ) ) C_ ( A X. A ) ) ) )
70 60 62 69 mpbir2and 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( w i^i ( A X. A ) ) e. ~P u )
71 inelcm 
 |-  ( ( ( w i^i ( A X. A ) ) e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) /\ ( w i^i ( A X. A ) ) e. ~P u ) -> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) )
72 57 70 71 syl2anc 
 |-  ( ( ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) /\ a e. RR+ ) /\ w = ( `' D " ( 0 [,) a ) ) ) -> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) )
73 simplr 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) -> w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) )
74 eqid 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
75 74 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) ) )
76 75 elv 
 |-  ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
77 73 76 sylib 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) -> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
78 33 39 72 77 r19.29af2 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) /\ w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) /\ w C_ v ) -> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) )
79 ssn0 
 |-  ( ( A C_ X /\ A =/= (/) ) -> X =/= (/) )
80 79 ancoms 
 |-  ( ( A =/= (/) /\ A C_ X ) -> X =/= (/) )
81 80 3adant2 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> X =/= (/) )
82 metuel 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( v e. ( metUnif ` D ) <-> ( v C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ v ) ) )
83 81 43 82 syl2anc 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( v e. ( metUnif ` D ) <-> ( v C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ v ) ) )
84 83 simplbda 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) -> E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ v )
85 84 adantr 
 |-  ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) -> E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ v )
86 78 85 r19.29a 
 |-  ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ v e. ( metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) ) -> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) )
87 86 r19.29an 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) ) -> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) )
88 26 87 jca 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) ) -> ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) )
89 simprl 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> u e. ~P ( A X. A ) )
90 89 elpwid 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> u C_ ( A X. A ) )
91 simpl3 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> A C_ X )
92 xpss12 
 |-  ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
93 91 91 92 syl2anc 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> ( A X. A ) C_ ( X X. X ) )
94 90 93 sstrd 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> u C_ ( X X. X ) )
95 difssd 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> ( ( X X. X ) \ ( A X. A ) ) C_ ( X X. X ) )
96 94 95 unssd 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> ( u u. ( ( X X. X ) \ ( A X. A ) ) ) C_ ( X X. X ) )
97 simplr 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> b e. RR+ )
98 eqidd 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) b ) ) )
99 4 imaeq2d 
 |-  ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
100 99 rspceeqv 
 |-  ( ( b e. RR+ /\ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) b ) ) ) -> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) )
101 97 98 100 syl2anc 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) )
102 43 ad4antr 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> D e. ( PsMet ` X ) )
103 cnvexg 
 |-  ( D e. ( PsMet ` X ) -> `' D e. _V )
104 imaexg 
 |-  ( `' D e. _V -> ( `' D " ( 0 [,) b ) ) e. _V )
105 74 elrnmpt 
 |-  ( ( `' D " ( 0 [,) b ) ) e. _V -> ( ( `' D " ( 0 [,) b ) ) e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) ) )
106 102 103 104 105 4syl 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( ( `' D " ( 0 [,) b ) ) e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) ) )
107 101 106 mpbird 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( `' D " ( 0 [,) b ) ) e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) )
108 cnvimass 
 |-  ( `' D " ( 0 [,) b ) ) C_ dom D
109 108 44 fssdm 
 |-  ( D e. ( PsMet ` X ) -> ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) )
110 102 109 syl 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) )
111 ssdif0 
 |-  ( ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) <-> ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) = (/) )
112 110 111 sylib 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) = (/) )
113 0ss 
 |-  (/) C_ u
114 112 113 eqsstrdi 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) C_ u )
115 respreima 
 |-  ( Fun D -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) = ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
116 102 44 45 115 4syl 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) = ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
117 simpr 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
118 simpllr 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> v e. ~P u )
119 118 elpwid 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> v C_ u )
120 117 119 eqsstrrd 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) C_ u )
121 116 120 eqsstrrd 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) C_ u )
122 114 121 unssd 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) u. ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) ) C_ u )
123 ssundif 
 |-  ( ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) <-> ( ( `' D " ( 0 [,) b ) ) \ u ) C_ ( ( X X. X ) \ ( A X. A ) ) )
124 difcom 
 |-  ( ( ( `' D " ( 0 [,) b ) ) \ u ) C_ ( ( X X. X ) \ ( A X. A ) ) <-> ( ( `' D " ( 0 [,) b ) ) \ ( ( X X. X ) \ ( A X. A ) ) ) C_ u )
125 difdif2 
 |-  ( ( `' D " ( 0 [,) b ) ) \ ( ( X X. X ) \ ( A X. A ) ) ) = ( ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) u. ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
126 125 sseq1i 
 |-  ( ( ( `' D " ( 0 [,) b ) ) \ ( ( X X. X ) \ ( A X. A ) ) ) C_ u <-> ( ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) u. ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) ) C_ u )
127 123 124 126 3bitri 
 |-  ( ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) <-> ( ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) u. ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) ) C_ u )
128 122 127 sylibr 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) )
129 sseq1 
 |-  ( w = ( `' D " ( 0 [,) b ) ) -> ( w C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) <-> ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) ) )
130 129 rspcev 
 |-  ( ( ( `' D " ( 0 [,) b ) ) e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) /\ ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) ) -> E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) )
131 107 128 130 syl2anc 
 |-  ( ( ( ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) /\ v e. ~P u ) /\ b e. RR+ ) /\ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) -> E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) )
132 elin 
 |-  ( v e. ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) <-> ( v e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) /\ v e. ~P u ) )
133 6 elrnmpt 
 |-  ( v e. _V -> ( v e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) <-> E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) )
134 133 elv 
 |-  ( v e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) <-> E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
135 134 anbi1i 
 |-  ( ( v e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) /\ v e. ~P u ) <-> ( E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) /\ v e. ~P u ) )
136 ancom 
 |-  ( ( E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) /\ v e. ~P u ) <-> ( v e. ~P u /\ E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) )
137 132 135 136 3bitri 
 |-  ( v e. ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) <-> ( v e. ~P u /\ E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) )
138 137 exbii 
 |-  ( E. v v e. ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) <-> E. v ( v e. ~P u /\ E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) )
139 n0 
 |-  ( ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) <-> E. v v e. ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) )
140 df-rex 
 |-  ( E. v e. ~P u E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) <-> E. v ( v e. ~P u /\ E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) ) )
141 138 139 140 3bitr4i 
 |-  ( ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) <-> E. v e. ~P u E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
142 141 biimpi 
 |-  ( ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) -> E. v e. ~P u E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
143 142 ad2antll 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> E. v e. ~P u E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
144 131 143 r19.29vva 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) )
145 81 adantr 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> X =/= (/) )
146 43 adantr 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> D e. ( PsMet ` X ) )
147 metuel 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) e. ( metUnif ` D ) <-> ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) ) ) )
148 145 146 147 syl2anc 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) e. ( metUnif ` D ) <-> ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) ) ) )
149 96 144 148 mpbir2and 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> ( u u. ( ( X X. X ) \ ( A X. A ) ) ) e. ( metUnif ` D ) )
150 indir 
 |-  ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) = ( ( u i^i ( A X. A ) ) u. ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) ) )
151 incom 
 |-  ( ( A X. A ) i^i ( ( X X. X ) \ ( A X. A ) ) ) = ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) )
152 disjdif 
 |-  ( ( A X. A ) i^i ( ( X X. X ) \ ( A X. A ) ) ) = (/)
153 151 152 eqtr3i 
 |-  ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) ) = (/)
154 153 uneq2i 
 |-  ( ( u i^i ( A X. A ) ) u. ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) ) ) = ( ( u i^i ( A X. A ) ) u. (/) )
155 un0 
 |-  ( ( u i^i ( A X. A ) ) u. (/) ) = ( u i^i ( A X. A ) )
156 150 154 155 3eqtri 
 |-  ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) = ( u i^i ( A X. A ) )
157 df-ss 
 |-  ( u C_ ( A X. A ) <-> ( u i^i ( A X. A ) ) = u )
158 90 157 sylib 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> ( u i^i ( A X. A ) ) = u )
159 156 158 syl5req 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> u = ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) )
160 ineq1 
 |-  ( v = ( u u. ( ( X X. X ) \ ( A X. A ) ) ) -> ( v i^i ( A X. A ) ) = ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) )
161 160 rspceeqv 
 |-  ( ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) e. ( metUnif ` D ) /\ u = ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) ) -> E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) )
162 149 159 161 syl2anc 
 |-  ( ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) /\ ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) -> E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) )
163 88 162 impbida 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) <-> ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) ) )
164 eqid 
 |-  ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) = ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) )
165 164 elrnmpt 
 |-  ( u e. _V -> ( u e. ran ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) <-> E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) ) )
166 165 elv 
 |-  ( u e. ran ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) <-> E. v e. ( metUnif ` D ) u = ( v i^i ( A X. A ) ) )
167 pweq 
 |-  ( v = u -> ~P v = ~P u )
168 167 ineq2d 
 |-  ( v = u -> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) = ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) )
169 168 neeq1d 
 |-  ( v = u -> ( ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) <-> ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) )
170 169 elrab 
 |-  ( u e. { v e. ~P ( A X. A ) | ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) } <-> ( u e. ~P ( A X. A ) /\ ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/) ) )
171 163 166 170 3bitr4g 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( u e. ran ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) <-> u e. { v e. ~P ( A X. A ) | ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) } ) )
172 171 eqrdv 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ran ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) = { v e. ~P ( A X. A ) | ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) } )
173 18 172 eqtrd 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( ( metUnif ` D ) |`t ( A X. A ) ) = { v e. ~P ( A X. A ) | ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P v ) =/= (/) } )
174 11 13 173 3eqtr4rd 
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( ( metUnif ` D ) |`t ( A X. A ) ) = ( metUnif ` ( D |` ( A X. A ) ) ) )