Theorem cfilucfil 22364

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 23063. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)

Hypothesis

Ref	Expression
metust.1	|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )

Assertion

Ref	Expression
cfilucfil	|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )

Distinct variable groups:   D, a   X, a   F, a, x   x, D, y   x, F, y   x, X, y, a   y, D   C, a, x, y

Proof of Theorem cfilucfil

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

Step	Hyp	Ref	Expression
1		metust.1	. . . . 5 |- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2	1	metust 22363	. . . 4 |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. (UnifOn ` X ) )
3		cfilufbas 22093	. . . 4 |- ( ( ( ( X X. X ) filGen F ) e. (UnifOn ` X ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) -> C e. ( fBas ` X ) )
4	2, 3	sylan 488	. . 3 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) -> C e. ( fBas ` X ) )
5		simpllr 799	. . . . . 6 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> D e. (PsMet ` X ) )
6		psmetf 22111	. . . . . 6 |- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
7		ffun 6048	. . . . . 6 |- ( D : ( X X. X ) --> RR* -> Fun D )
8	5, 6, 7	3syl 18	. . . . 5 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> Fun D )
9	2	ad2antrr 762	. . . . . 6 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( ( X X. X ) filGen F ) e. (UnifOn ` X ) )
10		simplr 792	. . . . . 6 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> C e. (CauFilu ` ( ( X X. X ) filGen F ) ) )
11	1	metustfbas 22362	. . . . . . . 8 |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )
12	11	ad2antrr 762	. . . . . . 7 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> F e. ( fBas ` ( X X. X ) ) )
13		cnvimass 5485	. . . . . . . 8 |- ( `' D " ( 0 [,) x ) ) C_ dom D
14		fdm 6051	. . . . . . . . 9 |- ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
15	5, 6, 14	3syl 18	. . . . . . . 8 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> dom D = ( X X. X ) )
16	13, 15	syl5sseq 3653	. . . . . . 7 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) x ) ) C_ ( X X. X ) )
17		simpr 477	. . . . . . . . . . 11 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> x e. RR+ )
18	17	rphalfcld 11884	. . . . . . . . . 10 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
19		eqidd 2623	. . . . . . . . . 10 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) )
20		oveq2 6658	. . . . . . . . . . . . 13 |- ( a = ( x / 2 ) -> ( 0 [,) a ) = ( 0 [,) ( x / 2 ) ) )
21	20	imaeq2d 5466	. . . . . . . . . . . 12 |- ( a = ( x / 2 ) -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) )
22	21	eqeq2d 2632	. . . . . . . . . . 11 |- ( a = ( x / 2 ) -> ( ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) <-> ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) ) )
23	22	rspcev 3309	. . . . . . . . . 10 |- ( ( ( x / 2 ) e. RR+ /\ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) ) -> E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) )
24	18, 19, 23	syl2anc 693	. . . . . . . . 9 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) )
25	1	metustel 22355	. . . . . . . . . 10 |- ( D e. (PsMet ` X ) -> ( ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F <-> E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) ) )
26	25	biimpar 502	. . . . . . . . 9 |- ( ( D e. (PsMet ` X ) /\ E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F )
27	5, 24, 26	syl2anc 693	. . . . . . . 8 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F )
28		0xr 10086	. . . . . . . . . . 11 |- 0 e. RR*
29	28	a1i 11	. . . . . . . . . 10 |- ( x e. RR+ -> 0 e. RR* )
30		rpxr 11840	. . . . . . . . . 10 |- ( x e. RR+ -> x e. RR* )
31		0le0 11110	. . . . . . . . . . 11 |- 0 <_ 0
32	31	a1i 11	. . . . . . . . . 10 |- ( x e. RR+ -> 0 <_ 0 )
33		rpre 11839	. . . . . . . . . . . 12 |- ( x e. RR+ -> x e. RR )
34	33	rehalfcld 11279	. . . . . . . . . . 11 |- ( x e. RR+ -> ( x / 2 ) e. RR )
35		rphalflt 11860	. . . . . . . . . . 11 |- ( x e. RR+ -> ( x / 2 ) < x )
36	34, 33, 35	ltled 10185	. . . . . . . . . 10 |- ( x e. RR+ -> ( x / 2 ) <_ x )
37		icossico 12243	. . . . . . . . . 10 |- ( ( ( 0 e. RR* /\ x e. RR* ) /\ ( 0 <_ 0 /\ ( x / 2 ) <_ x ) ) -> ( 0 [,) ( x / 2 ) ) C_ ( 0 [,) x ) )
38	29, 30, 32, 36, 37	syl22anc 1327	. . . . . . . . 9 |- ( x e. RR+ -> ( 0 [,) ( x / 2 ) ) C_ ( 0 [,) x ) )
39		imass2 5501	. . . . . . . . 9 |- ( ( 0 [,) ( x / 2 ) ) C_ ( 0 [,) x ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) )
40	17, 38, 39	3syl 18	. . . . . . . 8 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) )
41		sseq1 3626	. . . . . . . . 9 |- ( w = ( `' D " ( 0 [,) ( x / 2 ) ) ) -> ( w C_ ( `' D " ( 0 [,) x ) ) <-> ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) ) )
42	41	rspcev 3309	. . . . . . . 8 |- ( ( ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F /\ ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) ) -> E. w e. F w C_ ( `' D " ( 0 [,) x ) ) )
43	27, 40, 42	syl2anc 693	. . . . . . 7 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. w e. F w C_ ( `' D " ( 0 [,) x ) ) )
44		elfg 21675	. . . . . . . 8 |- ( F e. ( fBas ` ( X X. X ) ) -> ( ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) <-> ( ( `' D " ( 0 [,) x ) ) C_ ( X X. X ) /\ E. w e. F w C_ ( `' D " ( 0 [,) x ) ) ) ) )
45	44	biimpar 502	. . . . . . 7 |- ( ( F e. ( fBas ` ( X X. X ) ) /\ ( ( `' D " ( 0 [,) x ) ) C_ ( X X. X ) /\ E. w e. F w C_ ( `' D " ( 0 [,) x ) ) ) ) -> ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) )
46	12, 16, 43, 45	syl12anc 1324	. . . . . 6 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) )
47		cfiluexsm 22094	. . . . . 6 |- ( ( ( ( X X. X ) filGen F ) e. (UnifOn ` X ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) /\ ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) )
48	9, 10, 46, 47	syl3anc 1326	. . . . 5 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) )
49		funimass2 5972	. . . . . . 7 |- ( ( Fun D /\ ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) ) -> ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
50	49	ex 450	. . . . . 6 |- ( Fun D -> ( ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) -> ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
51	50	reximdv 3016	. . . . 5 |- ( Fun D -> ( E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
52	8, 48, 51	sylc 65	. . . 4 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
53	52	ralrimiva 2966	. . 3 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) -> A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
54	4, 53	jca 554	. 2 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ C e. (CauFilu ` ( ( X X. X ) filGen F ) ) ) -> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
55		simprl 794	. . 3 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> C e. ( fBas ` X ) )
56		simp-4r 807	. . . . . . . . 9 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
57	56	simprd 479	. . . . . . . 8 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
58		simplr 792	. . . . . . . 8 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> a e. RR+ )
59		oveq2 6658	. . . . . . . . . . 11 |- ( x = a -> ( 0 [,) x ) = ( 0 [,) a ) )
60	59	sseq2d 3633	. . . . . . . . . 10 |- ( x = a -> ( ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> ( D " ( y X. y ) ) C_ ( 0 [,) a ) ) )
61	60	rexbidv 3052	. . . . . . . . 9 |- ( x = a -> ( E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) ) )
62	61	rspccv 3306	. . . . . . . 8 |- ( A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) -> ( a e. RR+ -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) ) )
63	57, 58, 62	sylc 65	. . . . . . 7 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) )
64		nfv 1843	. . . . . . . . . . . 12 |- F/ y ( X =/= (/) /\ D e. (PsMet ` X ) )
65		nfv 1843	. . . . . . . . . . . . 13 |- F/ y C e. ( fBas ` X )
66		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ y RR+
67		nfre1 3005	. . . . . . . . . . . . . 14 |- F/ y E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x )
68	66, 67	nfral 2945	. . . . . . . . . . . . 13 |- F/ y A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x )
69	65, 68	nfan 1828	. . . . . . . . . . . 12 |- F/ y ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
70	64, 69	nfan 1828	. . . . . . . . . . 11 |- F/ y ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
71		nfv 1843	. . . . . . . . . . 11 |- F/ y v e. ( ( X X. X ) filGen F )
72	70, 71	nfan 1828	. . . . . . . . . 10 |- F/ y ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) )
73		nfv 1843	. . . . . . . . . 10 |- F/ y a e. RR+
74	72, 73	nfan 1828	. . . . . . . . 9 |- F/ y ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ )
75		nfv 1843	. . . . . . . . 9 |- F/ y ( `' D " ( 0 [,) a ) ) C_ v
76	74, 75	nfan 1828	. . . . . . . 8 |- F/ y ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v )
77	55	ad4antr 768	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> C e. ( fBas ` X ) )
78		fbelss 21637	. . . . . . . . . . . 12 |- ( ( C e. ( fBas ` X ) /\ y e. C ) -> y C_ X )
79	77, 78	sylancom 701	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> y C_ X )
80		xpss12 5225	. . . . . . . . . . 11 |- ( ( y C_ X /\ y C_ X ) -> ( y X. y ) C_ ( X X. X ) )
81	79, 79, 80	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> ( y X. y ) C_ ( X X. X ) )
82		simp-6r 811	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> D e. (PsMet ` X ) )
83	82, 6, 14	3syl 18	. . . . . . . . . 10 |- ( ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> dom D = ( X X. X ) )
84	81, 83	sseqtr4d 3642	. . . . . . . . 9 |- ( ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> ( y X. y ) C_ dom D )
85	84	ex 450	. . . . . . . 8 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> ( y e. C -> ( y X. y ) C_ dom D ) )
86	76, 85	ralrimi 2957	. . . . . . 7 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> A. y e. C ( y X. y ) C_ dom D )
87		r19.29r 3073	. . . . . . . 8 |- ( ( E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ A. y e. C ( y X. y ) C_ dom D ) -> E. y e. C ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) )
88		sseqin2 3817	. . . . . . . . . . . . 13 |- ( ( y X. y ) C_ dom D <-> ( dom D i^i ( y X. y ) ) = ( y X. y ) )
89	88	biimpi 206	. . . . . . . . . . . 12 |- ( ( y X. y ) C_ dom D -> ( dom D i^i ( y X. y ) ) = ( y X. y ) )
90	89	adantl 482	. . . . . . . . . . 11 |- ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( dom D i^i ( y X. y ) ) = ( y X. y ) )
91		dminss 5547	. . . . . . . . . . 11 |- ( dom D i^i ( y X. y ) ) C_ ( `' D " ( D " ( y X. y ) ) )
92	90, 91	syl6eqssr 3656	. . . . . . . . . 10 |- ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( y X. y ) C_ ( `' D " ( D " ( y X. y ) ) ) )
93		imass2 5501	. . . . . . . . . . 11 |- ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) -> ( `' D " ( D " ( y X. y ) ) ) C_ ( `' D " ( 0 [,) a ) ) )
94	93	adantr 481	. . . . . . . . . 10 |- ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( `' D " ( D " ( y X. y ) ) ) C_ ( `' D " ( 0 [,) a ) ) )
95	92, 94	sstrd 3613	. . . . . . . . 9 |- ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
96	95	reximi 3011	. . . . . . . 8 |- ( E. y e. C ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
97	87, 96	syl 17	. . . . . . 7 |- ( ( E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ A. y e. C ( y X. y ) C_ dom D ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
98	63, 86, 97	syl2anc 693	. . . . . 6 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
99		r19.41v 3089	. . . . . . 7 |- ( E. y e. C ( ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) <-> ( E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) )
100		sstr 3611	. . . . . . . 8 |- ( ( ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> ( y X. y ) C_ v )
101	100	reximi 3011	. . . . . . 7 |- ( E. y e. C ( ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ v )
102	99, 101	sylbir 225	. . . . . 6 |- ( ( E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ v )
103	98, 102	sylancom 701	. . . . 5 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ v )
104		simp-5r 809	. . . . . . . 8 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> D e. (PsMet ` X ) )
105		simplr 792	. . . . . . . 8 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> w e. F )
106	1	metustel 22355	. . . . . . . . 9 |- ( D e. (PsMet ` X ) -> ( w e. F <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) ) )
107	106	biimpa 501	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ w e. F ) -> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
108	104, 105, 107	syl2anc 693	. . . . . . 7 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
109		r19.41v 3089	. . . . . . . 8 |- ( E. a e. RR+ ( w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) <-> ( E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) )
110		sseq1 3626	. . . . . . . . . 10 |- ( w = ( `' D " ( 0 [,) a ) ) -> ( w C_ v <-> ( `' D " ( 0 [,) a ) ) C_ v ) )
111	110	biimpa 501	. . . . . . . . 9 |- ( ( w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) -> ( `' D " ( 0 [,) a ) ) C_ v )
112	111	reximi 3011	. . . . . . . 8 |- ( E. a e. RR+ ( w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
113	109, 112	sylbir 225	. . . . . . 7 |- ( ( E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
114	108, 113	sylancom 701	. . . . . 6 |- ( ( ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
115	11	ad2antrr 762	. . . . . . . 8 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> F e. ( fBas ` ( X X. X ) ) )
116		elfg 21675	. . . . . . . . 9 |- ( F e. ( fBas ` ( X X. X ) ) -> ( v e. ( ( X X. X ) filGen F ) <-> ( v C_ ( X X. X ) /\ E. w e. F w C_ v ) ) )
117	116	biimpa 501	. . . . . . . 8 |- ( ( F e. ( fBas ` ( X X. X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( v C_ ( X X. X ) /\ E. w e. F w C_ v ) )
118	115, 117	sylancom 701	. . . . . . 7 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( v C_ ( X X. X ) /\ E. w e. F w C_ v ) )
119	118	simprd 479	. . . . . 6 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. w e. F w C_ v )
120	114, 119	r19.29a 3078	. . . . 5 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
121	103, 120	r19.29a 3078	. . . 4 |- ( ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. y e. C ( y X. y ) C_ v )
122	121	ralrimiva 2966	. . 3 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> A. v e. ( ( X X. X ) filGen F ) E. y e. C ( y X. y ) C_ v )
123	2	adantr 481	. . . 4 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> ( ( X X. X ) filGen F ) e. (UnifOn ` X ) )
124		iscfilu 22092	. . . 4 |- ( ( ( X X. X ) filGen F ) e. (UnifOn ` X ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. v e. ( ( X X. X ) filGen F ) E. y e. C ( y X. y ) C_ v ) ) )
125	123, 124	syl 17	. . 3 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. v e. ( ( X X. X ) filGen F ) E. y e. C ( y X. y ) C_ v ) ) )
126	55, 122, 125	mpbir2and 957	. 2 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> C e. (CauFilu ` ( ( X X. X ) filGen F ) ) )
127	54, 126	impbida 877	1 |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   i^i cin 3573   C_ wss 3574   (/)c0 3915   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fun wfun 5882   -->wf 5884   ` cfv 5888  (class class class)co 6650   0cc0 9936   RR*cxr 10073   <_ cle 10075   / cdiv 10684   2c2 11070   RR+crp 11832   [,)cico 12177  PsMetcpsmet 19730   fBascfbas 19734   filGencfg 19735  UnifOncust 22003  CauFil_uccfilu 22090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-2 11079  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ico 12181  df-psmet 19738  df-fbas 19743  df-fg 19744  df-fil 21650  df-ust 22004  df-cfilu 22091

This theorem is referenced by:  cfilucfil2  22366