Theorem restmetu 18570

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

Assertion

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

Proof of Theorem restmetu

Dummy variables a b u v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 957	. . . 4 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> A =/= (/) )
2		psmetres2 18298	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ A C_ X ) -> ( D |` ( A X. A ) ) e. (PsMet ` A ) )
3	2	3adant1 975	. . . 4 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( D |` ( A X. A ) ) e. (PsMet ` A ) )
4		oveq2 6048	. . . . . . . 8 |- ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
5	4	imaeq2d 5162	. . . . . . 7 |- ( a = b -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
6	5	cbvmptv 4260	. . . . . 6 |- ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ( b e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
7	6	rneqi 5055	. . . . 5 |- ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ran ( b e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
8	7	metustfbas 18549	. . . 4 |- ( ( 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 643	. . 3 |- ( ( 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 17855	. . 3 |- ( 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 16	. 2 |- ( ( 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 18533	. . 3 |- ( ( 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 16	. 2 |- ( ( 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 5701	. . . 4 |- (metUnif ` D ) e. _V
15	3	elfvexd 5718	. . . . 5 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> A e. _V )
16		xpexg 4948	. . . . 5 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
17	15, 15, 16	syl2anc 643	. . . 4 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
18		restval 13609	. . . 4 |- ( ( (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 ) ) ) )
19	14, 17, 18	sylancr 645	. . 3 |- ( ( 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 ) ) ) )
20		inss2 3522	. . . . . . . . . . 11 |- ( v i^i ( A X. A ) ) C_ ( A X. A )
21		sseq1 3329	. . . . . . . . . . 11 |- ( u = ( v i^i ( A X. A ) ) -> ( u C_ ( A X. A ) <-> ( v i^i ( A X. A ) ) C_ ( A X. A ) ) )
22	20, 21	mpbiri 225	. . . . . . . . . 10 |- ( u = ( v i^i ( A X. A ) ) -> u C_ ( A X. A ) )
23		vex 2919	. . . . . . . . . . 11 |- u e. _V
24	23	elpw 3765	. . . . . . . . . 10 |- ( u e. ~P ( A X. A ) <-> u C_ ( A X. A ) )
25	22, 24	sylibr 204	. . . . . . . . 9 |- ( u = ( v i^i ( A X. A ) ) -> u e. ~P ( A X. A ) )
26	25	rexlimivw 2786	. . . . . . . 8 |- ( E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) ) -> u e. ~P ( A X. A ) )
27	26	adantl 453	. . . . . . 7 |- ( ( ( 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 ) )
28		nfv 1626	. . . . . . . . 9 |- F/ v ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X )
29		nfre1 2722	. . . . . . . . 9 |- F/ v E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) )
30	28, 29	nfan 1842	. . . . . . . 8 |- F/ v ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) /\ E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) ) )
31		nfv 1626	. . . . . . . . . . . . 13 |- F/ a ( ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) /\ v e. (metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) )
32		nfmpt1 4258	. . . . . . . . . . . . . . 15 |- F/_ a ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
33	32	nfrn 5071	. . . . . . . . . . . . . 14 |- F/_ a ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
34	33	nfcri 2534	. . . . . . . . . . . . 13 |- F/ a w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
35	31, 34	nfan 1842	. . . . . . . . . . . 12 |- 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 ) ) ) )
36		nfv 1626	. . . . . . . . . . . 12 |- F/ a w C_ v
37	35, 36	nfan 1842	. . . . . . . . . . 11 |- 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 )
38		nfmpt1 4258	. . . . . . . . . . . . . 14 |- F/_ a ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
39	38	nfrn 5071	. . . . . . . . . . . . 13 |- F/_ a ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
40		nfcv 2540	. . . . . . . . . . . . 13 |- F/_ a ~P u
41	39, 40	nfin 3507	. . . . . . . . . . . 12 |- F/_ a ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u )
42		nfcv 2540	. . . . . . . . . . . 12 |- F/_ a (/)
43	41, 42	nfne 2658	. . . . . . . . . . 11 |- F/ a ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/)
44		simplr 732	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( 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+ )
45		ineq1 3495	. . . . . . . . . . . . . . . 16 |- ( w = ( `' D " ( 0 [,) a ) ) -> ( w i^i ( A X. A ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
46	45	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( 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 ) ) )
47		simp2 958	. . . . . . . . . . . . . . . . 17 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> D e. (PsMet ` X ) )
48		psmetf 18290	. . . . . . . . . . . . . . . . . 18 |- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
49		ffun 5552	. . . . . . . . . . . . . . . . . 18 |- ( D : ( X X. X ) --> RR* -> Fun D )
50		respreima 5818	. . . . . . . . . . . . . . . . . 18 |- ( Fun D -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
51	48, 49, 50	3syl 19	. . . . . . . . . . . . . . . . 17 |- ( D e. (PsMet ` X ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
52	47, 51	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
53	52	ad6antr 717	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( 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 ) ) )
54	46, 53	eqtr4d 2439	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( 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 ) ) )
55		rspe 2727	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
56	44, 54, 55	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 ) ) )
57		vex 2919	. . . . . . . . . . . . . . 15 |- w e. _V
58	57	inex1 4304	. . . . . . . . . . . . . 14 |- ( w i^i ( A X. A ) ) e. _V
59		eqid 2404	. . . . . . . . . . . . . . 15 |- ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
60	59	elrnmpt 5076	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
61	58, 60	ax-mp 8	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
62	56, 61	sylibr 204	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( 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 ) ) ) )
63		simpllr 736	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( 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 )
64		ssinss1 3529	. . . . . . . . . . . . . 14 |- ( w C_ v -> ( w i^i ( A X. A ) ) C_ v )
65	63, 64	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 )
66		inss2 3522	. . . . . . . . . . . . . 14 |- ( w i^i ( A X. A ) ) C_ ( A X. A )
67	66	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 ) )
68		pweq 3762	. . . . . . . . . . . . . . . . 17 |- ( u = ( v i^i ( A X. A ) ) -> ~P u = ~P ( v i^i ( A X. A ) ) )
69	68	eleq2d 2471	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
70	58	elpw 3765	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
71	69, 70	syl6bb 253	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
72		ssin 3523	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
73	71, 72	syl6bbr 255	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
74	73	ad5antlr 716	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 ) ) ) )
75	65, 67, 74	mpbir2and 889	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( 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 )
76		inelcm 3642	. . . . . . . . . . . 12 |- ( ( ( 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 ) =/= (/) )
77	62, 75, 76	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( 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 ) =/= (/) )
78		simplr 732	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) ) ) )
79		eqid 2404	. . . . . . . . . . . . . 14 |- ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
80	79	elrnmpt 5076	. . . . . . . . . . . . 13 |- ( w e. _V -> ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) ) )
81	57, 80	ax-mp 8	. . . . . . . . . . . 12 |- ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
82	78, 81	sylib 189	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) )
83	37, 43, 77, 82	r19.29af2 2808	. . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) =/= (/) )
84		ssn0 3620	. . . . . . . . . . . . . . 15 |- ( ( A C_ X /\ A =/= (/) ) -> X =/= (/) )
85	84	ancoms 440	. . . . . . . . . . . . . 14 |- ( ( A =/= (/) /\ A C_ X ) -> X =/= (/) )
86	85	3adant2 976	. . . . . . . . . . . . 13 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> X =/= (/) )
87		metuel 18561	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
88	86, 47, 87	syl2anc 643	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
89	88	simplbda 608	. . . . . . . . . . 11 |- ( ( ( 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 )
90	89	adantr 452	. . . . . . . . . 10 |- ( ( ( ( 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 )
91	83, 90	r19.29a 2810	. . . . . . . . 9 |- ( ( ( ( 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 ) =/= (/) )
92	91	adantllr 700	. . . . . . . 8 |- ( ( ( ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) /\ E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) ) ) /\ 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 ) =/= (/) )
93		simpr 448	. . . . . . . 8 |- ( ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) /\ E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) ) ) -> E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) ) )
94	30, 92, 93	r19.29af 2809	. . . . . . 7 |- ( ( ( 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 ) =/= (/) )
95	27, 94	jca 519	. . . . . 6 |- ( ( ( 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 ) =/= (/) ) )
96		simprl 733	. . . . . . . . . . 11 |- ( ( ( 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 ) )
97	96	elpwid 3768	. . . . . . . . . 10 |- ( ( ( 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 ) )
98		simpl3 962	. . . . . . . . . . 11 |- ( ( ( 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 )
99		xpss12 4940	. . . . . . . . . . 11 |- ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
100	98, 98, 99	syl2anc 643	. . . . . . . . . 10 |- ( ( ( 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 ) )
101	97, 100	sstrd 3318	. . . . . . . . 9 |- ( ( ( 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 ) )
102		difssd 3435	. . . . . . . . 9 |- ( ( ( 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 ) )
103	101, 102	unssd 3483	. . . . . . . 8 |- ( ( ( 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 ) )
104		simplr 732	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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+ )
105		eqidd 2405	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) ) )
106	4	imaeq2d 5162	. . . . . . . . . . . . . 14 |- ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
107	106	eqeq2d 2415	. . . . . . . . . . . . 13 |- ( a = b -> ( ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) <-> ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) b ) ) ) )
108	107	rspcev 3012	. . . . . . . . . . . 12 |- ( ( b e. RR+ /\ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) b ) ) ) -> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) )
109	104, 105, 108	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) )
110	47	ad4antr 713	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) )
111		cnvexg 5364	. . . . . . . . . . . . 13 |- ( D e. (PsMet ` X ) -> `' D e. _V )
112		imaexg 5176	. . . . . . . . . . . . 13 |- ( `' D e. _V -> ( `' D " ( 0 [,) b ) ) e. _V )
113	79	elrnmpt 5076	. . . . . . . . . . . . 13 |- ( ( `' 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 ) ) ) )
114	111, 112, 113	3syl 19	. . . . . . . . . . . 12 |- ( D e. (PsMet ` X ) -> ( ( `' D " ( 0 [,) b ) ) e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) ) )
115	110, 114	syl 16	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) ) )
116	109, 115	mpbird 224	. . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) ) ) )
117		cnvimass 5183	. . . . . . . . . . . . . . . 16 |- ( `' D " ( 0 [,) b ) ) C_ dom D
118		fdm 5554	. . . . . . . . . . . . . . . . 17 |- ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
119	48, 118	syl 16	. . . . . . . . . . . . . . . 16 |- ( D e. (PsMet ` X ) -> dom D = ( X X. X ) )
120	117, 119	syl5sseq 3356	. . . . . . . . . . . . . . 15 |- ( D e. (PsMet ` X ) -> ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) )
121	110, 120	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
122		ssdif0 3646	. . . . . . . . . . . . . 14 |- ( ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) <-> ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) = (/) )
123	121, 122	sylib 189	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) = (/) )
124		0ss 3616	. . . . . . . . . . . . 13 |- (/) C_ u
125	123, 124	syl6eqss 3358	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
126		respreima 5818	. . . . . . . . . . . . . . 15 |- ( Fun D -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) = ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
127	48, 49, 126	3syl 19	. . . . . . . . . . . . . 14 |- ( D e. (PsMet ` X ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) = ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
128	110, 127	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) )
129		simpr 448	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
130		simpllr 736	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
131	130	elpwid 3768	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
132	129, 131	eqsstr3d 3343	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
133	128, 132	eqsstr3d 3343	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
134	125, 133	unssd 3483	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 )
135		ssundif 3671	. . . . . . . . . . . 12 |- ( ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) <-> ( ( `' D " ( 0 [,) b ) ) \ u ) C_ ( ( X X. X ) \ ( A X. A ) ) )
136		difcom 3672	. . . . . . . . . . . 12 |- ( ( ( `' D " ( 0 [,) b ) ) \ u ) C_ ( ( X X. X ) \ ( A X. A ) ) <-> ( ( `' D " ( 0 [,) b ) ) \ ( ( X X. X ) \ ( A X. A ) ) ) C_ u )
137		difdif2 3558	. . . . . . . . . . . . 13 |- ( ( `' D " ( 0 [,) b ) ) \ ( ( X X. X ) \ ( A X. A ) ) ) = ( ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) u. ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
138	137	sseq1i 3332	. . . . . . . . . . . 12 |- ( ( ( `' 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 )
139	135, 136, 138	3bitri 263	. . . . . . . . . . 11 |- ( ( `' 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 )
140	134, 139	sylibr 204	. . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) ) ) )
141		sseq1 3329	. . . . . . . . . . 11 |- ( 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 ) ) ) ) )
142	141	rspcev 3012	. . . . . . . . . 10 |- ( ( ( `' 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 ) ) ) )
143	116, 140, 142	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( ( ( 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 ) ) ) )
144		elin 3490	. . . . . . . . . . . . . 14 |- ( 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 ) )
145		vex 2919	. . . . . . . . . . . . . . . 16 |- v e. _V
146	6	elrnmpt 5076	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
147	145, 146	ax-mp 8	. . . . . . . . . . . . . . 15 |- ( v e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) <-> E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
148	147	anbi1i 677	. . . . . . . . . . . . . 14 |- ( ( 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 ) )
149		ancom 438	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
150	144, 148, 149	3bitri 263	. . . . . . . . . . . . 13 |- ( 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 ) ) ) )
151	150	exbii 1589	. . . . . . . . . . . 12 |- ( 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 ) ) ) )
152		n0 3597	. . . . . . . . . . . 12 |- ( ( 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 ) )
153		df-rex 2672	. . . . . . . . . . . 12 |- ( 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 ) ) ) )
154	151, 152, 153	3bitr4i 269	. . . . . . . . . . 11 |- ( ( 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 ) ) )
155	154	biimpi 187	. . . . . . . . . 10 |- ( ( 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 ) ) )
156	155	ad2antll 710	. . . . . . . . 9 |- ( ( ( 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 ) ) )
157	143, 156	r19.29_2a 2812	. . . . . . . 8 |- ( ( ( 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 ) ) ) )
158	86	adantr 452	. . . . . . . . 9 |- ( ( ( 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 =/= (/) )
159	47	adantr 452	. . . . . . . . 9 |- ( ( ( 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 ) )
160		metuel 18561	. . . . . . . . 9 |- ( ( 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 ) ) ) ) ) )
161	158, 159, 160	syl2anc 643	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) ) )
162	103, 157, 161	mpbir2and 889	. . . . . . 7 |- ( ( ( 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 ) )
163		indir 3549	. . . . . . . . 9 |- ( ( 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 ) ) )
164		incom 3493	. . . . . . . . . . 11 |- ( ( A X. A ) i^i ( ( X X. X ) \ ( A X. A ) ) ) = ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) )
165		disjdif 3660	. . . . . . . . . . 11 |- ( ( A X. A ) i^i ( ( X X. X ) \ ( A X. A ) ) ) = (/)
166	164, 165	eqtr3i 2426	. . . . . . . . . 10 |- ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) ) = (/)
167	166	uneq2i 3458	. . . . . . . . 9 |- ( ( 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. (/) )
168		un0 3612	. . . . . . . . 9 |- ( ( u i^i ( A X. A ) ) u. (/) ) = ( u i^i ( A X. A ) )
169	163, 167, 168	3eqtri 2428	. . . . . . . 8 |- ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) = ( u i^i ( A X. A ) )
170		df-ss 3294	. . . . . . . . 9 |- ( u C_ ( A X. A ) <-> ( u i^i ( A X. A ) ) = u )
171	97, 170	sylib 189	. . . . . . . 8 |- ( ( ( 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 )
172	169, 171	syl5req 2449	. . . . . . 7 |- ( ( ( 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 ) ) )
173		ineq1 3495	. . . . . . . . 9 |- ( 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 ) ) )
174	173	eqeq2d 2415	. . . . . . . 8 |- ( v = ( u u. ( ( X X. X ) \ ( A X. A ) ) ) -> ( u = ( v i^i ( A X. A ) ) <-> u = ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) ) )
175	174	rspcev 3012	. . . . . . 7 |- ( ( ( 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 ) ) )
176	162, 172, 175	syl2anc 643	. . . . . 6 |- ( ( ( 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 ) ) )
177	95, 176	impbida 806	. . . . 5 |- ( ( 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 ) =/= (/) ) ) )
178		eqid 2404	. . . . . . 7 |- ( v e. (metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) = ( v e. (metUnif ` D ) |-> ( v i^i ( A X. A ) ) )
179	178	elrnmpt 5076	. . . . . 6 |- ( 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 ) ) ) )
180	23, 179	ax-mp 8	. . . . 5 |- ( 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 ) ) )
181		pweq 3762	. . . . . . . 8 |- ( v = u -> ~P v = ~P u )
182	181	ineq2d 3502	. . . . . . 7 |- ( 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 ) )
183	182	neeq1d 2580	. . . . . 6 |- ( 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 ) =/= (/) ) )
184	183	elrab 3052	. . . . 5 |- ( 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 ) =/= (/) ) )
185	177, 180, 184	3bitr4g 280	. . . 4 |- ( ( 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 ) =/= (/) } ) )
186	185	eqrdv 2402	. . 3 |- ( ( 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 ) =/= (/) } )
187	19, 186	eqtrd 2436	. 2 |- ( ( 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 ) =/= (/) } )
188	11, 13, 187	3eqtr4rd 2447	1 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( (metUnif ` D ) ↾t ( A X. A ) ) = (metUnif ` ( D |` ( A X. A ) ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2567   E.wrex 2667   {crab 2670   _Vcvv 2916   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   (/)c0 3588   ~Pcpw 3759   e. cmpt 4226   X. cxp 4835   `'ccnv 4836   dom cdm 4837   ran crn 4838   |` cres 4839   "cima 4840   Fun wfun 5407   -->wf 5409   ` cfv 5413  (class class class)co 6040   0cc0 8946   RR*cxr 9075   RR+crp 10568   [,)cico 10874   ↾_t crest 13603  PsMetcpsmet 16640   fBascfbas 16644   filGencfg 16645  metUnifcmetu 16648

This theorem is referenced by:  reust  24297  qqhucn  24329  rrhre  24340

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-po 4463  df-so 4464  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-rp 10569  df-ico 10878  df-rest 13605  df-psmet 16649  df-fbas 16654  df-fg 16655  df-metu 16657