Theorem metcnpi3 21610

Description: Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 21609 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)

Hypotheses

Ref	Expression
metcn.2	|- J = ( MetOpen ` C )
metcn.4	|- K = ( MetOpen ` D )

Assertion

Ref	Expression
metcnpi3	|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )

Distinct variable groups:   x, y, F   x, J, y   x, K, y   x, X, y   x, Y, y   x, A, y   x, C, y   x, D, y   x, P, y

Proof of Theorem metcnpi3

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		metcn.2	. . 3 |- J = ( MetOpen ` C )
2		metcn.4	. . 3 |- K = ( MetOpen ` D )
3	1, 2	metcnpi2 21609	. 2 |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. z e. RR+ A. y e. X ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) )
4		rphalfcl 11356	. . . 4 |- ( z e. RR+ -> ( z / 2 ) e. RR+ )
5	4	ad2antrl 739	. . 3 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ A. y e. X ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) ) ) -> ( z / 2 ) e. RR+ )
6		simplll 773	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> C e. ( *Met ` X ) )
7		simprr 771	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> y e. X )
8		simplrl 775	. . . . . . . . . . 11 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> F e. ( ( J CnP K ) ` P ) )
9		eqid 2462	. . . . . . . . . . . 12 |- U. J = U. J
10	9	cnprcl 20310	. . . . . . . . . . 11 |- ( F e. ( ( J CnP K ) ` P ) -> P e. U. J )
11	8, 10	syl 17	. . . . . . . . . 10 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> P e. U. J )
12	1	mopnuni 21505	. . . . . . . . . . 11 |- ( C e. ( *Met ` X ) -> X = U. J )
13	6, 12	syl 17	. . . . . . . . . 10 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> X = U. J )
14	11, 13	eleqtrrd 2543	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> P e. X )
15		xmetcl 21395	. . . . . . . . 9 |- ( ( C e. ( *Met ` X ) /\ y e. X /\ P e. X ) -> ( y C P ) e. RR* )
16	6, 7, 14, 15	syl3anc 1276	. . . . . . . 8 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( y C P ) e. RR* )
17	4	ad2antrl 739	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( z / 2 ) e. RR+ )
18	17	rpxrd 11371	. . . . . . . 8 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( z / 2 ) e. RR* )
19		rpxr 11338	. . . . . . . . 9 |- ( z e. RR+ -> z e. RR* )
20	19	ad2antrl 739	. . . . . . . 8 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> z e. RR* )
21		rphalflt 11358	. . . . . . . . 9 |- ( z e. RR+ -> ( z / 2 ) < z )
22	21	ad2antrl 739	. . . . . . . 8 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( z / 2 ) < z )
23		xrlelttr 11482	. . . . . . . . . 10 |- ( ( ( y C P ) e. RR* /\ ( z / 2 ) e. RR* /\ z e. RR* ) -> ( ( ( y C P ) <_ ( z / 2 ) /\ ( z / 2 ) < z ) -> ( y C P ) < z ) )
24	23	expcomd 444	. . . . . . . . 9 |- ( ( ( y C P ) e. RR* /\ ( z / 2 ) e. RR* /\ z e. RR* ) -> ( ( z / 2 ) < z -> ( ( y C P ) <_ ( z / 2 ) -> ( y C P ) < z ) ) )
25	24	imp 435	. . . . . . . 8 |- ( ( ( ( y C P ) e. RR* /\ ( z / 2 ) e. RR* /\ z e. RR* ) /\ ( z / 2 ) < z ) -> ( ( y C P ) <_ ( z / 2 ) -> ( y C P ) < z ) )
26	16, 18, 20, 22, 25	syl31anc 1279	. . . . . . 7 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( ( y C P ) <_ ( z / 2 ) -> ( y C P ) < z ) )
27		simpllr 774	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> D e. ( *Met ` Y ) )
28	1	mopntopon 21503	. . . . . . . . . . . 12 |- ( C e. ( *Met ` X ) -> J e. (TopOn ` X ) )
29	6, 28	syl 17	. . . . . . . . . . 11 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> J e. (TopOn ` X ) )
30	2	mopntopon 21503	. . . . . . . . . . . 12 |- ( D e. ( *Met ` Y ) -> K e. (TopOn ` Y ) )
31	27, 30	syl 17	. . . . . . . . . . 11 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> K e. (TopOn ` Y ) )
32		cnpf2 20315	. . . . . . . . . . 11 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
33	29, 31, 8, 32	syl3anc 1276	. . . . . . . . . 10 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> F : X --> Y )
34	33, 7	ffvelrnd 6046	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( F ` y ) e. Y )
35	33, 14	ffvelrnd 6046	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( F ` P ) e. Y )
36		xmetcl 21395	. . . . . . . . 9 |- ( ( D e. ( *Met ` Y ) /\ ( F ` y ) e. Y /\ ( F ` P ) e. Y ) -> ( ( F ` y ) D ( F ` P ) ) e. RR* )
37	27, 34, 35, 36	syl3anc 1276	. . . . . . . 8 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( ( F ` y ) D ( F ` P ) ) e. RR* )
38		simplrr 776	. . . . . . . . 9 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> A e. RR+ )
39	38	rpxrd 11371	. . . . . . . 8 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> A e. RR* )
40		xrltle 11477	. . . . . . . 8 |- ( ( ( ( F ` y ) D ( F ` P ) ) e. RR* /\ A e. RR* ) -> ( ( ( F ` y ) D ( F ` P ) ) < A -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
41	37, 39, 40	syl2anc 671	. . . . . . 7 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( ( ( F ` y ) D ( F ` P ) ) < A -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
42	26, 41	imim12d 77	. . . . . 6 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ y e. X ) ) -> ( ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) -> ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) ) )
43	42	anassrs 658	. . . . 5 |- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ z e. RR+ ) /\ y e. X ) -> ( ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) -> ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) ) )
44	43	ralimdva 2808	. . . 4 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ z e. RR+ ) -> ( A. y e. X ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) -> A. y e. X ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) ) )
45	44	impr 629	. . 3 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ A. y e. X ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) ) ) -> A. y e. X ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
46		breq2 4420	. . . . . 6 |- ( x = ( z / 2 ) -> ( ( y C P ) <_ x <-> ( y C P ) <_ ( z / 2 ) ) )
47	46	imbi1d 323	. . . . 5 |- ( x = ( z / 2 ) -> ( ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) <-> ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) ) )
48	47	ralbidv 2839	. . . 4 |- ( x = ( z / 2 ) -> ( A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) <-> A. y e. X ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) ) )
49	48	rspcev 3162	. . 3 |- ( ( ( z / 2 ) e. RR+ /\ A. y e. X ( ( y C P ) <_ ( z / 2 ) -> ( ( F ` y ) D ( F ` P ) ) <_ A ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
50	5, 45, 49	syl2anc 671	. 2 |- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) /\ ( z e. RR+ /\ A. y e. X ( ( y C P ) < z -> ( ( F ` y ) D ( F ` P ) ) < A ) ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
51	3, 50	rexlimddv 2895	1 |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   U.cuni 4212   class class class wbr 4416   -->wf 5597   ` cfv 5601  (class class class)co 6315   RR*cxr 9700   < clt 9701   <_ cle 9702   / cdiv 10297   2c2 10687   RR+crp 11331   *Metcxmt 19004   MetOpencmopn 19009  TopOnctopon 19967   CnP ccnp 20290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-map 7500  df-en 7596  df-dom 7597  df-sdom 7598  df-sup 7982  df-inf 7983  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-n0 10899  df-z 10967  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-topgen 15391  df-psmet 19011  df-xmet 19012  df-bl 19014  df-mopn 19015  df-top 19970  df-bases 19971  df-topon 19972  df-cnp 20293

This theorem is referenced by:  blocnilem  26494