Theorem restmetu 20818

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 991	. . . 4 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> A =/= (/) )
2		psmetres2 20546	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ A C_ X ) -> ( D |` ( A X. A ) ) e. (PsMet ` A ) )
3	2	3adant1 1009	. . . 4 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( D |` ( A X. A ) ) e. (PsMet ` A ) )
4		oveq2 6283	. . . . . . . 8 |- ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
5	4	imaeq2d 5328	. . . . . . 7 |- ( a = b -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
6	5	cbvmptv 4531	. . . . . 6 |- ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ( b e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
7	6	rneqi 5220	. . . . 5 |- ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ran ( b e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
8	7	metustfbas 20797	. . . 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 661	. . 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 20099	. . 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 20781	. . 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 5867	. . . 4 |- (metUnif ` D ) e. _V
15	3	elfvexd 5885	. . . . 5 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> A e. _V )
16		xpexg 6702	. . . . 5 |- ( ( A e. _V /\ A e. _V ) -> ( A X. A ) e. _V )
17	15, 15, 16	syl2anc 661	. . . 4 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( A X. A ) e. _V )
18		restval 14671	. . . 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 663	. . 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 3712	. . . . . . . . . . 11 |- ( v i^i ( A X. A ) ) C_ ( A X. A )
21		sseq1 3518	. . . . . . . . . . 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 233	. . . . . . . . . 10 |- ( u = ( v i^i ( A X. A ) ) -> u C_ ( A X. A ) )
23		vex 3109	. . . . . . . . . . 11 |- u e. _V
24	23	elpw 4009	. . . . . . . . . 10 |- ( u e. ~P ( A X. A ) <-> u C_ ( A X. A ) )
25	22, 24	sylibr 212	. . . . . . . . 9 |- ( u = ( v i^i ( A X. A ) ) -> u e. ~P ( A X. A ) )
26	25	rexlimivw 2945	. . . . . . . 8 |- ( E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) ) -> u e. ~P ( A X. A ) )
27	26	adantl 466	. . . . . . 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 1678	. . . . . . . . 9 |- F/ v ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X )
29		nfre1 2918	. . . . . . . . 9 |- F/ v E. v e. (metUnif ` D ) u = ( v i^i ( A X. A ) )
30	28, 29	nfan 1870	. . . . . . . 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 1678	. . . . . . . . . . . . 13 |- F/ a ( ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) /\ v e. (metUnif ` D ) ) /\ u = ( v i^i ( A X. A ) ) )
32		nfmpt1 4529	. . . . . . . . . . . . . . 15 |- F/_ a ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
33	32	nfrn 5236	. . . . . . . . . . . . . 14 |- F/_ a ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
34	33	nfcri 2615	. . . . . . . . . . . . 13 |- F/ a w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
35	31, 34	nfan 1870	. . . . . . . . . . . 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 1678	. . . . . . . . . . . 12 |- F/ a w C_ v
37	35, 36	nfan 1870	. . . . . . . . . . 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 4529	. . . . . . . . . . . . . 14 |- F/_ a ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
39	38	nfrn 5236	. . . . . . . . . . . . 13 |- F/_ a ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
40		nfcv 2622	. . . . . . . . . . . . 13 |- F/_ a ~P u
41	39, 40	nfin 3698	. . . . . . . . . . . 12 |- F/_ a ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u )
42		nfcv 2622	. . . . . . . . . . . 12 |- F/_ a (/)
43	41, 42	nfne 2791	. . . . . . . . . . 11 |- F/ a ( ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) i^i ~P u ) =/= (/)
44		simplr 754	. . . . . . . . . . . . . 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 3686	. . . . . . . . . . . . . . . 16 |- ( w = ( `' D " ( 0 [,) a ) ) -> ( w i^i ( A X. A ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
46	45	adantl 466	. . . . . . . . . . . . . . 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 992	. . . . . . . . . . . . . . . . 17 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> D e. (PsMet ` X ) )
48		psmetf 20538	. . . . . . . . . . . . . . . . 17 |- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
49		ffun 5724	. . . . . . . . . . . . . . . . 17 |- ( D : ( X X. X ) --> RR* -> Fun D )
50		respreima 6001	. . . . . . . . . . . . . . . . 17 |- ( Fun D -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
51	47, 48, 49, 50	4syl 21	. . . . . . . . . . . . . . . 16 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) = ( ( `' D " ( 0 [,) a ) ) i^i ( A X. A ) ) )
52	51	ad6antr 735	. . . . . . . . . . . . . . 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 ) ) )
53	46, 52	eqtr4d 2504	. . . . . . . . . . . . . 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 ) ) )
54		rspe 2915	. . . . . . . . . . . . . 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 ) ) )
55	44, 53, 54	syl2anc 661	. . . . . . . . . . . . 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 ) ) )
56		vex 3109	. . . . . . . . . . . . . . 15 |- w e. _V
57	56	inex1 4581	. . . . . . . . . . . . . 14 |- ( w i^i ( A X. A ) ) e. _V
58		eqid 2460	. . . . . . . . . . . . . . 15 |- ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) )
59	58	elrnmpt 5240	. . . . . . . . . . . . . 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 ) ) ) )
60	57, 59	ax-mp 5	. . . . . . . . . . . . 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 ) ) )
61	55, 60	sylibr 212	. . . . . . . . . . . 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 ) ) ) )
62		simpllr 758	. . . . . . . . . . . . . 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 )
63		ssinss1 3719	. . . . . . . . . . . . . 14 |- ( w C_ v -> ( w i^i ( A X. A ) ) C_ v )
64	62, 63	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 )
65		inss2 3712	. . . . . . . . . . . . . 14 |- ( w i^i ( A X. A ) ) C_ ( A X. A )
66	65	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 ) )
67		pweq 4006	. . . . . . . . . . . . . . . . 17 |- ( u = ( v i^i ( A X. A ) ) -> ~P u = ~P ( v i^i ( A X. A ) ) )
68	67	eleq2d 2530	. . . . . . . . . . . . . . . 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 ) ) ) )
69	57	elpw 4009	. . . . . . . . . . . . . . . 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 ) ) )
70	68, 69	syl6bb 261	. . . . . . . . . . . . . . 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 ) ) ) )
71		ssin 3713	. . . . . . . . . . . . . . 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 ) ) )
72	70, 71	syl6bbr 263	. . . . . . . . . . . . . 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 ) ) ) )
73	72	ad5antlr 734	. . . . . . . . . . . . 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 ) ) ) )
74	64, 66, 73	mpbir2and 915	. . . . . . . . . . . 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 )
75		inelcm 3874	. . . . . . . . . . . 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 ) =/= (/) )
76	61, 74, 75	syl2anc 661	. . . . . . . . . . 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 ) =/= (/) )
77		simplr 754	. . . . . . . . . . . 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 ) ) ) )
78		eqid 2460	. . . . . . . . . . . . . 14 |- ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
79	78	elrnmpt 5240	. . . . . . . . . . . . 13 |- ( w e. _V -> ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) ) )
80	56, 79	ax-mp 5	. . . . . . . . . . . 12 |- ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
81	77, 80	sylib 196	. . . . . . . . . . 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 ) ) )
82	37, 43, 76, 81	r19.29af2 2993	. . . . . . . . . 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 ) =/= (/) )
83		ssn0 3811	. . . . . . . . . . . . . . 15 |- ( ( A C_ X /\ A =/= (/) ) -> X =/= (/) )
84	83	ancoms 453	. . . . . . . . . . . . . 14 |- ( ( A =/= (/) /\ A C_ X ) -> X =/= (/) )
85	84	3adant2 1010	. . . . . . . . . . . . 13 |- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> X =/= (/) )
86		metuel 20809	. . . . . . . . . . . . 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 ) ) )
87	85, 47, 86	syl2anc 661	. . . . . . . . . . . 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 ) ) )
88	87	simplbda 624	. . . . . . . . . . 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 )
89	88	adantr 465	. . . . . . . . . 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 )
90	82, 89	r19.29a 2996	. . . . . . . . 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 ) =/= (/) )
91	90	adantllr 718	. . . . . . . 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 ) =/= (/) )
92		simpr 461	. . . . . . . 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 ) ) )
93	30, 91, 92	r19.29af 2994	. . . . . . 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 ) =/= (/) )
94	27, 93	jca 532	. . . . . 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 ) =/= (/) ) )
95		simprl 755	. . . . . . . . . . 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 ) )
96	95	elpwid 4013	. . . . . . . . . 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 ) )
97		simpl3 996	. . . . . . . . . . 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 )
98		xpss12 5099	. . . . . . . . . . 11 |- ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
99	97, 97, 98	syl2anc 661	. . . . . . . . . 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 ) )
100	96, 99	sstrd 3507	. . . . . . . . 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 ) )
101		difssd 3625	. . . . . . . . 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 ) )
102	100, 101	unssd 3673	. . . . . . . 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 ) )
103		simplr 754	. . . . . . . . . . . 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+ )
104		eqidd 2461	. . . . . . . . . . . 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 ) ) )
105	4	imaeq2d 5328	. . . . . . . . . . . . . 14 |- ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
106	105	eqeq2d 2474	. . . . . . . . . . . . 13 |- ( a = b -> ( ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) <-> ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) b ) ) ) )
107	106	rspcev 3207	. . . . . . . . . . . 12 |- ( ( b e. RR+ /\ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) b ) ) ) -> E. a e. RR+ ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) a ) ) )
108	103, 104, 107	syl2anc 661	. . . . . . . . . . 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 ) ) )
109	47	ad4antr 731	. . . . . . . . . . . 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 ) )
110		cnvexg 6720	. . . . . . . . . . . 12 |- ( D e. (PsMet ` X ) -> `' D e. _V )
111		imaexg 6711	. . . . . . . . . . . 12 |- ( `' D e. _V -> ( `' D " ( 0 [,) b ) ) e. _V )
112	78	elrnmpt 5240	. . . . . . . . . . . 12 |- ( ( `' 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 ) ) ) )
113	109, 110, 111, 112	4syl 21	. . . . . . . . . . 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 ) ) ) )
114	108, 113	mpbird 232	. . . . . . . . . 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 ) ) ) )
115		cnvimass 5348	. . . . . . . . . . . . . . . 16 |- ( `' D " ( 0 [,) b ) ) C_ dom D
116		fdm 5726	. . . . . . . . . . . . . . . . 17 |- ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
117	48, 116	syl 16	. . . . . . . . . . . . . . . 16 |- ( D e. (PsMet ` X ) -> dom D = ( X X. X ) )
118	115, 117	syl5sseq 3545	. . . . . . . . . . . . . . 15 |- ( D e. (PsMet ` X ) -> ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) )
119	109, 118	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 ) )
120		ssdif0 3878	. . . . . . . . . . . . . 14 |- ( ( `' D " ( 0 [,) b ) ) C_ ( X X. X ) <-> ( ( `' D " ( 0 [,) b ) ) \ ( X X. X ) ) = (/) )
121	119, 120	sylib 196	. . . . . . . . . . . . 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 ) ) = (/) )
122		0ss 3807	. . . . . . . . . . . . 13 |- (/) C_ u
123	121, 122	syl6eqss 3547	. . . . . . . . . . . 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 )
124		respreima 6001	. . . . . . . . . . . . . 14 |- ( Fun D -> ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) = ( ( `' D " ( 0 [,) b ) ) i^i ( A X. A ) ) )
125	109, 48, 49, 124	4syl 21	. . . . . . . . . . . . 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 ) ) )
126		simpr 461	. . . . . . . . . . . . . 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 ) ) )
127		simpllr 758	. . . . . . . . . . . . . . 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 )
128	127	elpwid 4013	. . . . . . . . . . . . . 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 )
129	126, 128	eqsstr3d 3532	. . . . . . . . . . . . 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 )
130	125, 129	eqsstr3d 3532	. . . . . . . . . . . 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 )
131	123, 130	unssd 3673	. . . . . . . . . . 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 )
132		ssundif 3903	. . . . . . . . . . . 12 |- ( ( `' D " ( 0 [,) b ) ) C_ ( u u. ( ( X X. X ) \ ( A X. A ) ) ) <-> ( ( `' D " ( 0 [,) b ) ) \ u ) C_ ( ( X X. X ) \ ( A X. A ) ) )
133		difcom 3904	. . . . . . . . . . . 12 |- ( ( ( `' D " ( 0 [,) b ) ) \ u ) C_ ( ( X X. X ) \ ( A X. A ) ) <-> ( ( `' D " ( 0 [,) b ) ) \ ( ( X X. X ) \ ( A X. A ) ) ) C_ u )
134		difdif2 3748	. . . . . . . . . . . . 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 ) ) )
135	134	sseq1i 3521	. . . . . . . . . . . 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 )
136	132, 133, 135	3bitri 271	. . . . . . . . . . 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 )
137	131, 136	sylibr 212	. . . . . . . . . 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 ) ) ) )
138		sseq1 3518	. . . . . . . . . . 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 ) ) ) ) )
139	138	rspcev 3207	. . . . . . . . . 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 ) ) ) )
140	114, 137, 139	syl2anc 661	. . . . . . . . 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 ) ) ) )
141		elin 3680	. . . . . . . . . . . . . 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 ) )
142		vex 3109	. . . . . . . . . . . . . . . 16 |- v e. _V
143	6	elrnmpt 5240	. . . . . . . . . . . . . . . 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 ) ) ) )
144	142, 143	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( v e. ran ( a e. RR+ |-> ( `' ( D |` ( A X. A ) ) " ( 0 [,) a ) ) ) <-> E. b e. RR+ v = ( `' ( D |` ( A X. A ) ) " ( 0 [,) b ) ) )
145	144	anbi1i 695	. . . . . . . . . . . . . 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 ) )
146		ancom 450	. . . . . . . . . . . . . 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 ) ) ) )
147	141, 145, 146	3bitri 271	. . . . . . . . . . . . 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 ) ) ) )
148	147	exbii 1639	. . . . . . . . . . . 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 ) ) ) )
149		n0 3787	. . . . . . . . . . . 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 ) )
150		df-rex 2813	. . . . . . . . . . . 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 ) ) ) )
151	148, 149, 150	3bitr4i 277	. . . . . . . . . . 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 ) ) )
152	151	biimpi 194	. . . . . . . . . 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 ) ) )
153	152	ad2antll 728	. . . . . . . . 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 ) ) )
154	140, 153	r19.29_2a 2998	. . . . . . . 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 ) ) ) )
155	85	adantr 465	. . . . . . . . 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 =/= (/) )
156	47	adantr 465	. . . . . . . . 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 ) )
157		metuel 20809	. . . . . . . . 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 ) ) ) ) ) )
158	155, 156, 157	syl2anc 661	. . . . . . . 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 ) ) ) ) ) )
159	102, 154, 158	mpbir2and 915	. . . . . . 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 ) )
160		indir 3739	. . . . . . . . 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 ) ) )
161		incom 3684	. . . . . . . . . . 11 |- ( ( A X. A ) i^i ( ( X X. X ) \ ( A X. A ) ) ) = ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) )
162		disjdif 3892	. . . . . . . . . . 11 |- ( ( A X. A ) i^i ( ( X X. X ) \ ( A X. A ) ) ) = (/)
163	161, 162	eqtr3i 2491	. . . . . . . . . 10 |- ( ( ( X X. X ) \ ( A X. A ) ) i^i ( A X. A ) ) = (/)
164	163	uneq2i 3648	. . . . . . . . 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. (/) )
165		un0 3803	. . . . . . . . 9 |- ( ( u i^i ( A X. A ) ) u. (/) ) = ( u i^i ( A X. A ) )
166	160, 164, 165	3eqtri 2493	. . . . . . . 8 |- ( ( u u. ( ( X X. X ) \ ( A X. A ) ) ) i^i ( A X. A ) ) = ( u i^i ( A X. A ) )
167		df-ss 3483	. . . . . . . . 9 |- ( u C_ ( A X. A ) <-> ( u i^i ( A X. A ) ) = u )
168	96, 167	sylib 196	. . . . . . . 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 )
169	166, 168	syl5req 2514	. . . . . . 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 ) ) )
170		ineq1 3686	. . . . . . . . 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 ) ) )
171	170	eqeq2d 2474	. . . . . . . 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 ) ) ) )
172	171	rspcev 3207	. . . . . . 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 ) ) )
173	159, 169, 172	syl2anc 661	. . . . . 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 ) ) )
174	94, 173	impbida 829	. . . . 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 ) =/= (/) ) ) )
175		eqid 2460	. . . . . . 7 |- ( v e. (metUnif ` D ) |-> ( v i^i ( A X. A ) ) ) = ( v e. (metUnif ` D ) |-> ( v i^i ( A X. A ) ) )
176	175	elrnmpt 5240	. . . . . 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 ) ) ) )
177	23, 176	ax-mp 5	. . . . 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 ) ) )
178		pweq 4006	. . . . . . . 8 |- ( v = u -> ~P v = ~P u )
179	178	ineq2d 3693	. . . . . . 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 ) )
180	179	neeq1d 2737	. . . . . 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 ) =/= (/) ) )
181	180	elrab 3254	. . . . 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 ) =/= (/) ) )
182	174, 177, 181	3bitr4g 288	. . . 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 ) =/= (/) } ) )
183	182	eqrdv 2457	. . 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 ) =/= (/) } )
184	19, 183	eqtrd 2501	. 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 ) =/= (/) } )
185	11, 13, 184	3eqtr4rd 2512	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 184   /\ wa 369   /\ w3a 968   = wceq 1374   E.wex 1591   e. wcel 1762   =/= wne 2655   E.wrex 2808   {crab 2811   _Vcvv 3106   \ cdif 3466   u. cun 3467   i^i cin 3468   C_ wss 3469   (/)c0 3778   ~Pcpw 4003   |-> cmpt 4498   X. cxp 4990   `'ccnv 4991   dom cdm 4992   ran crn 4993   |` cres 4994   "cima 4995   Fun wfun 5573   -->wf 5575   ` cfv 5579  (class class class)co 6275   0cc0 9481   RR*cxr 9616   RR+crp 11209   [,)cico 11520   ↾_t crest 14665  PsMetcpsmet 18166   fBascfbas 18170   filGencfg 18171  metUnifcmetu 18174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-po 4793  df-so 4794  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6774  df-2nd 6775  df-er 7301  df-map 7412  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-rp 11210  df-ico 11524  df-rest 14667  df-psmet 18175  df-fbas 18180  df-fg 18181  df-metu 18183

This theorem is referenced by:  reust  21541  qqhucn  27459