Theorem cnfnct 9849

Description: Basic continuity property of a continuous functional.

Assertion

Ref	Expression
cnfnct	|- (((T e. ConFn /\ A e. H~) /\ (B e. RR /\ 0 < B)) -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))

Distinct variable groups:   x,y,A   x,B,y   x,T,y

Proof of Theorem cnfnct

Step	Hyp	Ref	Expression
1		elcnfnt 9804	. . . 4 |- (T e. ConFn <-> (T:H~-->CC /\ A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w)))))
2	1	pm3.27bi 326	. . 3 |- (T e. ConFn -> A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w))))
3		opreq2 3975	. . . . . . . . . . . . 13 |- (z = A -> (y -h z) = (y -h A))
4	3	fveq2d 3734	. . . . . . . . . . . 12 |- (z = A -> (normh` (y -h z)) = (normh` (y -h A)))
5	4	breq1d 2634	. . . . . . . . . . 11 |- (z = A -> ((normh` (y -h z)) < x <-> (normh` (y -h A)) < x))
6		fveq2 3730	. . . . . . . . . . . . . 14 |- (z = A -> (T` z) = (T` A))
7	6	opreq2d 3982	. . . . . . . . . . . . 13 |- (z = A -> ((T` y) - (T` z)) = ((T` y) - (T` A)))
8	7	fveq2d 3734	. . . . . . . . . . . 12 |- (z = A -> (abs` ((T` y) - (T` z))) = (abs` ((T` y) - (T` A))))
9	8	breq1d 2634	. . . . . . . . . . 11 |- (z = A -> ((abs` ((T` y) - (T` z))) < w <-> (abs` ((T` y) - (T` A))) < w))
10	5, 9	imbi12d 628	. . . . . . . . . 10 |- (z = A -> (((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w) <-> ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)))
11	10	ralbidv 1666	. . . . . . . . 9 |- (z = A -> (A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w) <-> A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)))
12	11	anbi2d 618	. . . . . . . 8 |- (z = A -> ((0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w)) <-> (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w))))
13	12	rexbidv 1667	. . . . . . 7 |- (z = A -> (E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w)) <-> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w))))
14	13	imbi2d 614	. . . . . 6 |- (z = A -> ((0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w))) <-> (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)))))
15	14	ralbidv 1666	. . . . 5 |- (z = A -> (A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w))) <-> A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)))))
16	15	rcla4cv 1877	. . . 4 |- (A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w))) -> (A e. H~ -> A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)))))
17		breq2 2628	. . . . . 6 |- (w = B -> (0 < w <-> 0 < B))
18		breq2 2628	. . . . . . . . . 10 |- (w = B -> ((abs` ((T` y) - (T` A))) < w <-> (abs` ((T` y) - (T` A))) < B))
19	18	imbi2d 614	. . . . . . . . 9 |- (w = B -> (((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w) <-> ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))
20	19	ralbidv 1666	. . . . . . . 8 |- (w = B -> (A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w) <-> A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))
21	20	anbi2d 618	. . . . . . 7 |- (w = B -> ((0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)) <-> (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B))))
22	21	rexbidv 1667	. . . . . 6 |- (w = B -> (E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w)) <-> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B))))
23	17, 22	imbi12d 628	. . . . 5 |- (w = B -> ((0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w))) <-> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))))
24	23	rcla4cv 1877	. . . 4 |- (A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < w))) -> (B e. RR -> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))))
25	16, 24	syl6 22	. . 3 |- (A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (abs` ((T` y) - (T` z))) < w))) -> (A e. H~ -> (B e. RR -> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B))))))
26	2, 25	syl 10	. 2 |- (T e. ConFn -> (A e. H~ -> (B e. RR -> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B))))))
27	26	imp43 370	1 |- (((T e. ConFn /\ A e. H~) /\ (B e. RR /\ 0 < B)) -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (abs` ((T` y) - (T` A))) < B)))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960  A.wral 1648  E.wrex 1649   class class class wbr 2624  -->wf 3184  ` cfv 3188  (class class class)co 3969  CCcc 5244  RRcr 5245  0cc0 5246   - cmin 5304   < clt 5498  abscabs 6751  H~chil