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 disjdifr
 |-  ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) ) = (/)
152 151 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. (/) )
153 un0
 |-  ( ( u i^i ( A X. A ) ) u. (/) ) = ( u i^i ( A X. A ) )
154 150 152 153 3eqtri
 |-  ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) = ( u i^i ( A X. A ) )
155 df-ss
 |-  ( u C_ ( A X. A ) <-> ( u i^i ( A X. A ) ) = u )
156 90 155 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 )
157 154 156 eqtr2id
 |-  ( ( ( 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 ) ) )
158 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 ) ) )
159 158 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 ) ) )
160 149 157 159 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 ) ) )
161 88 160 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 ) =/= (/) ) ) )
162 eqid
 |-  ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) = ( v e. ( metUnif ` D ) |-> ( v i^i ( A X. A ) ) )
163 162 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 ) ) ) )
164 163 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 ) ) )
165 pweq
 |-  ( v = u -> ~P v = ~P u )
166 165 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 ) )
167 166 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 ) =/= (/) ) )
168 167 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 ) =/= (/) ) )
169 161 164 168 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 ) =/= (/) } ) )
170 169 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 ) =/= (/) } )
171 18 170 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 ) =/= (/) } )
172 11 13 171 3eqtr4rd
 |-  ( ( A =/= (/) /\ D e. ( PsMet ` X ) /\ A C_ X ) -> ( ( metUnif ` D ) |`t ( A X. A ) ) = ( metUnif ` ( D |` ( A X. A ) ) ) )