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 ) ) ) ) |