Theorem metcnpi4 10037

Description: Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi 10034 with non-strict ordering.

Hypotheses

Ref	Expression
metcn.1	|- X = dom dom C
metcn.2	|- J = (MetOpen` C)
metcn.3	|- Y = dom dom D
metcn.4	|- K = (MetOpen` D)

Assertion

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

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

Proof of Theorem metcnpi4

Step	Hyp	Ref	Expression
1		metcn.1	. . 3 |- X = dom dom C
2		metcn.2	. . 3 |- J = (MetOpen` C)
3		metcn.3	. . 3 |- Y = dom dom D
4		metcn.4	. . 3 |- K = (MetOpen` D)
5	1, 2, 3, 4	metcnpi 10034	. 2 |- (((C e. Met /\ D e. Met /\ P e. X) /\ (F e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)))
6	1, 3, 2, 4	metcnpf 10027	. . . . 5 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F e. ((J CnP K)` P)) -> F:X-->Y)
7		rehalfcl 7560	. . . . . . . . . 10 |- (z e. RR -> (z / 2) e. RR)
8	7	ad2antrl 804	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)))) -> (z / 2) e. RR)
9	1	metcl 9954	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. Met /\ P e. X /\ y e. X) -> (PCy) e. RR)
10		halfpos 7562	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> (0 < z <-> (z / 2) < z))
11	10	biimpa 615	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ 0 < z) -> (z / 2) < z)
12	11	adantl 448	. . . . . . . . . . . . . . . . . . . . . 22 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> (z / 2) < z)
13		simpl 437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ z e. RR) -> (PCy) e. RR)
14	7	adantl 448	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ z e. RR) -> (z / 2) e. RR)
15		simpr 442	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ z e. RR) -> z e. RR)
16		lelttr 6882	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ (z / 2) e. RR /\ z e. RR) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
17	13, 14, 15, 16	syl111anc 1349	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((PCy) e. RR /\ z e. RR) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
18	17	adantrr 781	. . . . . . . . . . . . . . . . . . . . . 22 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
19	12, 18	mpan2d 683	. . . . . . . . . . . . . . . . . . . . 21 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> ((PCy) <_ (z / 2) -> (PCy) < z))
20	19	ex 398	. . . . . . . . . . . . . . . . . . . 20 |- ((PCy) e. RR -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z)))
21	9, 20	syl 13	. . . . . . . . . . . . . . . . . . 19 |- ((C e. Met /\ P e. X /\ y e. X) -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z)))
22	21	3expia 1319	. . . . . . . . . . . . . . . . . 18 |- ((C e. Met /\ P e. X) -> (y e. X -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z))))
23	22	com23 65	. . . . . . . . . . . . . . . . 17 |- ((C e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
24	23	3adant2 1139	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ D e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
25	24	ad2antrr 799	. . . . . . . . . . . . . . 15 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
26	25	imp31 396	. . . . . . . . . . . . . 14 |- ((((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) /\ y e. X) -> ((PCy) <_ (z / 2) -> (PCy) < z))
27		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:X-->Y /\ P e. X) -> (F` P) e. Y)
28		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:X-->Y /\ y e. X) -> (F` y) e. Y)
29	27, 28	anim12i 536	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F:X-->Y /\ P e. X) /\ (F:X-->Y /\ y e. X)) -> ((F` P) e. Y /\ (F` y) e. Y))
30	29	anandis 889	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->Y /\ (P e. X /\ y e. X)) -> ((F` P) e. Y /\ (F` y) e. Y))
31	3	metcl 9954	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ (F` P) e. Y /\ (F` y) e. Y) -> ((F` P)D(F` y)) e. RR)
32	31	3expb 1318	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D e. Met /\ ((F` P) e. Y /\ (F` y) e. Y)) -> ((F` P)D(F` y)) e. RR)
33	30, 32	sylan2 600	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ (F:X-->Y /\ (P e. X /\ y e. X))) -> ((F` P)D(F` y)) e. RR)
34	33	exp45 588	. . . . . . . . . . . . . . . . . . . . 21 |- (D e. Met -> (F:X-->Y -> (P e. X -> (y e. X -> ((F` P)D(F` y)) e. RR))))
35	34	com23 65	. . . . . . . . . . . . . . . . . . . 20 |- (D e. Met -> (P e. X -> (F:X-->Y -> (y e. X -> ((F` P)D(F` y)) e. RR))))
36	35	imp 393	. . . . . . . . . . . . . . . . . . 19 |- ((D e. Met /\ P e. X) -> (F:X-->Y -> (y e. X -> ((F` P)D(F` y)) e. RR)))
37	36	3adant1 1138	. . . . . . . . . . . . . . . . . 18 |- ((C e. Met /\ D e. Met /\ P e. X) -> (F:X-->Y -> (y e. X -> ((F` P)D(F` y)) e. RR)))
38	37	imp31 396	. . . . . . . . . . . . . . . . 17 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ y e. X) -> ((F` P)D(F` y)) e. RR)
39	38	adantlr 777	. . . . . . . . . . . . . . . 16 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ y e. X) -> ((F` P)D(F` y)) e. RR)
40		simplrl 816	. . . . . . . . . . . . . . . 16 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ y e. X) -> A e. RR)
41		ltle 6879	. . . . . . . . . . . . . . . 16 |- ((((F` P)D(F` y)) e. RR /\ A e. RR) -> (((F` P)D(F` y)) < A -> ((F` P)D(F` y)) <_ A))
42	39, 40, 41	syl11anc 659	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ y e. X) -> (((F` P)D(F` y)) < A -> ((F` P)D(F` y)) <_ A))
43	42	adantlr 777	. . . . . . . . . . . . . 14 |- ((((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) /\ y e. X) -> (((F` P)D(F` y)) < A -> ((F` P)D(F` y)) <_ A))
44	26, 43	imim12d 61	. . . . . . . . . . . . 13 |- ((((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) /\ y e. X) -> (((PCy) < z -> ((F` P)D(F` y)) < A) -> ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
45	44	ralimdva 2421	. . . . . . . . . . . 12 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) -> (A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A) -> A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
46		halfpos2 7563	. . . . . . . . . . . . . 14 |- (z e. RR -> (0 < z <-> 0 < (z / 2)))
47	46	biimpa 615	. . . . . . . . . . . . 13 |- ((z e. RR /\ 0 < z) -> 0 < (z / 2))
48	47	adantl 448	. . . . . . . . . . . 12 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) -> 0 < (z / 2))
49	45, 48	jctild 507	. . . . . . . . . . 11 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) -> (A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A) -> (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A))))
50	49	exp32 578	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) -> (z e. RR -> (0 < z -> (A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A) -> (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A))))))
51	50	imp45 573	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)))) -> (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
52		breq2 3511	. . . . . . . . . . 11 |- (x = (z / 2) -> (0 < x <-> 0 < (z / 2)))
53		breq2 3511	. . . . . . . . . . . . 13 |- (x = (z / 2) -> ((PCy) <_ x <-> (PCy) <_ (z / 2)))
54	53	imbi1d 748	. . . . . . . . . . . 12 |- (x = (z / 2) -> (((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
55	54	ralbidv 2373	. . . . . . . . . . 11 |- (x = (z / 2) -> (A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
56	52, 55	anbi12d 763	. . . . . . . . . 10 |- (x = (z / 2) -> ((0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)) <-> (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A))))
57	56	rcla4ev 2620	. . . . . . . . 9 |- (((z / 2) e. RR /\ (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A))) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))
58	8, 51, 57	syl11anc 659	. . . . . . . 8 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)))) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))
59	58	exp32 578	. . . . . . 7 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) -> (z e. RR -> ((0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))))
60	59	r19.23adv 2463	. . . . . 6 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) -> (E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
61	60	exp32 578	. . . . 5 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) -> (A e. RR -> (0 < A -> (E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))))
62	6, 61	syldan 595	. . . 4 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F e. ((J CnP K)` P)) -> (A e. RR -> (0 < A -> (E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))))
63	62	ex 398	. . 3 |- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) -> (A e. RR -> (0 < A -> (E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))))))
64	63	3imp2 1332	. 2 |- (((C e. Met /\ D e. Met /\ P e. X) /\ (F e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> (E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
65	5, 64	mpd 11	1 |- (((C e. Met /\ D e. Met /\ P e. X) /\ (F e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))

Syntax hints:   -> wi 3   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  A.wral 2355  E.wrex 2356   class class class wbr 3507  dom cdm 4119  -->wf 4127  ` cfv 4131  (class class class)co 4981  RRcr 6751  0cc0 6752   <_ cle 6841   < clt 6845   / cdiv 6991  2c2 7478   CnP ccnp 9895  Metcme 9932  MetOpencopn 9935

This theorem is referenced by:  nvcnpi4 10631

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-map 5544  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-2 7487  df-top 9692  df-cnp 9897  df-met 9936  df-bl 9938  df-opn 9939

Copyright terms: Public domain