Theorem metustbl 20814

Description: The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.)

Assertion

Ref	Expression
metustbl	|- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) )

Distinct variable groups:   D, a   P, a   V, a   X, a

Proof of Theorem metustbl

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

Step	Hyp	Ref	Expression
1		simp1 991	. . 3 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> D e. (PsMet ` X ) )
2		simp3 993	. . 3 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> P e. X )
3		simpr 461	. . . . 5 |- ( ( ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) /\ w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) ) /\ w C_ V ) -> w C_ V )
4		vex 3111	. . . . . . . 8 |- w e. _V
5		eqid 2462	. . . . . . . . 9 |- ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) = ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) )
6	5	elrnmpt 5242	. . . . . . . 8 |- ( w e. _V -> ( w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) <-> E. r e. RR+ w = ( `' D " ( 0 [,) r ) ) ) )
7	4, 6	ax-mp 5	. . . . . . 7 |- ( w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) <-> E. r e. RR+ w = ( `' D " ( 0 [,) r ) ) )
8	7	biimpi 194	. . . . . 6 |- ( w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) -> E. r e. RR+ w = ( `' D " ( 0 [,) r ) ) )
9	8	ad2antlr 726	. . . . 5 |- ( ( ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) /\ w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) ) /\ w C_ V ) -> E. r e. RR+ w = ( `' D " ( 0 [,) r ) ) )
10		sseq1 3520	. . . . . . . 8 |- ( w = ( `' D " ( 0 [,) r ) ) -> ( w C_ V <-> ( `' D " ( 0 [,) r ) ) C_ V ) )
11	10	biimpcd 224	. . . . . . 7 |- ( w C_ V -> ( w = ( `' D " ( 0 [,) r ) ) -> ( `' D " ( 0 [,) r ) ) C_ V ) )
12	11	reximdv 2932	. . . . . 6 |- ( w C_ V -> ( E. r e. RR+ w = ( `' D " ( 0 [,) r ) ) -> E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V ) )
13	12	imp 429	. . . . 5 |- ( ( w C_ V /\ E. r e. RR+ w = ( `' D " ( 0 [,) r ) ) ) -> E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V )
14	3, 9, 13	syl2anc 661	. . . 4 |- ( ( ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) /\ w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) ) /\ w C_ V ) -> E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V )
15		ne0i 3786	. . . . . 6 |- ( P e. X -> X =/= (/) )
16	2, 15	syl 16	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> X =/= (/) )
17		simp2 992	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> V e. (metUnif ` D ) )
18		metuel 20811	. . . . . 6 |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( V e. (metUnif ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) w C_ V ) ) )
19	18	simplbda 624	. . . . 5 |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ V e. (metUnif ` D ) ) -> E. w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) w C_ V )
20	16, 1, 17, 19	syl21anc 1222	. . . 4 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. w e. ran ( r e. RR+ |-> ( `' D " ( 0 [,) r ) ) ) w C_ V )
21	14, 20	r19.29a 2998	. . 3 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V )
22		imass1 5364	. . . . . 6 |- ( ( `' D " ( 0 [,) r ) ) C_ V -> ( ( `' D " ( 0 [,) r ) ) " { P } ) C_ ( V " { P } ) )
23	22	reximi 2927	. . . . 5 |- ( E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V -> E. r e. RR+ ( ( `' D " ( 0 [,) r ) ) " { P } ) C_ ( V " { P } ) )
24		blval2 20808	. . . . . . . 8 |- ( ( D e. (PsMet ` X ) /\ P e. X /\ r e. RR+ ) -> ( P ( ball ` D ) r ) = ( ( `' D " ( 0 [,) r ) ) " { P } ) )
25	24	sseq1d 3526	. . . . . . 7 |- ( ( D e. (PsMet ` X ) /\ P e. X /\ r e. RR+ ) -> ( ( P ( ball ` D ) r ) C_ ( V " { P } ) <-> ( ( `' D " ( 0 [,) r ) ) " { P } ) C_ ( V " { P } ) ) )
26	25	3expa 1191	. . . . . 6 |- ( ( ( D e. (PsMet ` X ) /\ P e. X ) /\ r e. RR+ ) -> ( ( P ( ball ` D ) r ) C_ ( V " { P } ) <-> ( ( `' D " ( 0 [,) r ) ) " { P } ) C_ ( V " { P } ) ) )
27	26	rexbidva 2965	. . . . 5 |- ( ( D e. (PsMet ` X ) /\ P e. X ) -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ ( V " { P } ) <-> E. r e. RR+ ( ( `' D " ( 0 [,) r ) ) " { P } ) C_ ( V " { P } ) ) )
28	23, 27	syl5ibr 221	. . . 4 |- ( ( D e. (PsMet ` X ) /\ P e. X ) -> ( E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V -> E. r e. RR+ ( P ( ball ` D ) r ) C_ ( V " { P } ) ) )
29	28	imp 429	. . 3 |- ( ( ( D e. (PsMet ` X ) /\ P e. X ) /\ E. r e. RR+ ( `' D " ( 0 [,) r ) ) C_ V ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ ( V " { P } ) )
30	1, 2, 21, 29	syl21anc 1222	. 2 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ ( V " { P } ) )
31		blssexps 20659	. . 3 |- ( ( D e. (PsMet ` X ) /\ P e. X ) -> ( E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ ( V " { P } ) ) )
32	31	3adant2 1010	. 2 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> ( E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ ( V " { P } ) ) )
33	30, 32	mpbird 232	1 |- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 968   = wceq 1374   e. wcel 1762   =/= wne 2657   E.wrex 2810   _Vcvv 3108   C_ wss 3471   (/)c0 3780   {csn 4022   |-> cmpt 4500   X. cxp 4992   `'ccnv 4993   ran crn 4995   "cima 4997   ` cfv 5581  (class class class)co 6277   0cc0 9483   RR+crp 11211   [,)cico 11522  PsMetcpsmet 18168   ballcbl 18171  metUnifcmetu 18176

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 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560  ax-pre-sup 9561

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 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-reu 2816  df-rmo 2817  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-uni 4241  df-iun 4322  df-br 4443  df-opab 4501  df-mpt 4502  df-tr 4536  df-eprel 4786  df-id 4790  df-po 4795  df-so 4796  df-fr 4833  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6674  df-1st 6776  df-2nd 6777  df-recs 7034  df-rdg 7068  df-er 7303  df-map 7414  df-en 7509  df-dom 7510  df-sdom 7511  df-sup 7892  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9798  df-neg 9799  df-div 10198  df-nn 10528  df-2 10585  df-n0 10787  df-z 10856  df-uz 11074  df-q 11174  df-rp 11212  df-xneg 11309  df-xadd 11310  df-xmul 11311  df-ico 11526  df-psmet 18177  df-bl 18180  df-fbas 18182  df-fg 18183  df-metu 18185

This theorem is referenced by:  psmetutop  20816