Theorem ubthlem6 8534

Description: Lemma for ubthi 8544. Using bcth 8032 (via bcthlem33 8031), at least one set A` k contains a ball.

Hypotheses

Ref	Expression
ubthlem4.1	|- X = (Base` U)
ubthlem4.2	|- Y = (Base` W)
ubthlem4.3	|- N = (norm` W)
ubthlem4.5	|- B = (U BLnOp W)
ubthlem4.6	|- T:NN-->B
ubthlem4.7	|- U e. CBan
ubthlem4.8	|- W e. NrmCVec
ubthlem4.9	|- D = (IndMet` U)
ubthlem4.10	|- J = (Open` D)
ubthlem4.11	|- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}

Assertion

Ref	Expression
ubthlem6	|- (A.x e. X E.c e. RR A.n e. NN (N` ((T` n)` x)) <_ c -> E.k e. NN E.p e. X E.r e. RR (0 < r /\ (p( ball ` D)r) (_ (A` k)))

Distinct variable groups:   k,c,n,p,r,x,A   D,k,n,r,x   k,J,p,r,x   h,j,k,n,y,z,N   T,h,j,k,n,y,z   j,c,y,z,X,x,k,n   x,h

Proof of Theorem ubthlem6

Step	Hyp	Ref	Expression
1		ubthlem4.1	. . . . 5 |- X = (Base` U)
2		ubthlem4.2	. . . . 5 |- Y = (Base` W)
3		ubthlem4.3	. . . . 5 |- N = (norm` W)
4		ubthlem4.5	. . . . 5 |- B = (U BLnOp W)
5		ubthlem4.6	. . . . 5 |- T:NN-->B
6		ubthlem4.7	. . . . 5 |- U e. CBan
7		ubthlem4.8	. . . . 5 |- W e. NrmCVec
8		ubthlem4.9	. . . . 5 |- D = (IndMet` U)
9		ubthlem4.10	. . . . 5 |- J = (Open` D)
10		ubthlem4.11	. . . . 5 |- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	ubthlem5 8533	. . . 4 |- (A.x e. X E.c e. RR A.n e. NN (N` ((T` n)` x)) <_ c -> U_k e. NN (A` k) = X)
12		fvex 3732	. . . . . . . 8 |- (Base` U) e. V
13	1, 12	eqeltr 1544	. . . . . . 7 |- X e. V
14	13	rabex 2725	. . . . . 6 |- {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j} e. V
15	14, 10	fnopab2 3618	. . . . 5 |- A Fn NN
16		fniunfv 3865	. . . . 5 |- (A Fn NN -> U_k e. NN (A` k) = U.ran A)
17	15, 16	ax-mp 7	. . . 4 |- U_k e. NN (A` k) = U.ran A
18	11, 17	syl5eqr 1521	. . 3 |- (A.x e. X E.c e. RR A.n e. NN (N` ((T` n)` x)) <_ c -> U.ran A = X)
19		fvelrnb 3760	. . . . . . 7 |- (A Fn NN -> (x e. ran A <-> E.k e. NN (A` k) = x))
20	15, 19	ax-mp 7	. . . . . 6 |- (x e. ran A <-> E.k e. NN (A` k) = x)
21		pm3.27 323	. . . . . . . 8 |- ((k e. NN /\ (A` k) = x) -> (A` k) = x)
22	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	ubthlem4 8532	. . . . . . . . 9 |- (k e. NN -> (A` k) e. (Clsd` J))
23	22	adantr 389	. . . . . . . 8 |- ((k e. NN /\ (A` k) = x) -> (A` k) e. (Clsd` J))
24	21, 23	eqeltrrd 1549	. . . . . . 7 |- ((k e. NN /\ (A` k) = x) -> x e. (Clsd` J))
25	24	r19.23aiva 1744	. . . . . 6 |- (E.k e. NN (A` k) = x -> x e. (Clsd` J))
26	20, 25	sylbi 199	. . . . 5 |- (x e. ran A -> x e. (Clsd` J))
27	26	ssriv 2069	. . . 4 |- ran A (_ (Clsd` J)
28	8	bncms 8525	. . . . . 6 |- (U e. CBan -> D e. CMet)
29	6, 28	ax-mp 7	. . . . 5 |- D e. CMet
30		bnnv 8526	. . . . . . . 8 |- (U e. CBan -> U e. NrmCVec)
31	6, 30	ax-mp 7	. . . . . . 7 |- U e. NrmCVec
32		eqid 1475	. . . . . . . 8 |- (0v` U) = (0v` U)
33	1, 32	nvzcl 8255	. . . . . . 7 |- (U e. NrmCVec -> (0v` U) e. X)
34	31, 33	ax-mp 7	. . . . . 6 |- (0v` U) e. X
35		ne0i 2286	. . . . . 6 |- ((0v` U) e. X -> X =/= (/))
36	34, 35	ax-mp 7	. . . . 5 |- X =/= (/)
37	1, 8, 31	imsbai 8322	. . . . 5 |- X = dom dom D
38		ffnfv 3828	. . . . . 6 |- (A:NN-->P~X <-> (A Fn NN /\ A.k e. NN (A` k) e. P~X))
39	1, 10	ubthlem2 8530	. . . . . . . 8 |- (k e. NN -> (A` k) (_ X)
40		fvex 3732	. . . . . . . . 9 |- (A` k) e. V
41	40	elpw 2404	. . . . . . . 8 |- ((A` k) e. P~X <-> (A` k) (_ X)
42	39, 41	sylibr 200	. . . . . . 7 |- (k e. NN -> (A` k) e. P~X)
43	42	rgen 1698	. . . . . 6 |- A.k e. NN (A` k) e. P~X
44	38, 15, 43	mpbir2an 730	. . . . 5 |- A:NN-->P~X
45	29, 36, 37, 9, 44	bcthlem33 8031	. . . 4 |- ((U.ran A = X /\ ran A (_ (Clsd` J)) -> E.k e. NN ((int` J)` (A` k)) =/= (/))
46	27, 45	mpan2 696	. . 3 |- (U.ran A = X -> E.k e. NN ((int` J)` (A` k)) =/= (/))
47	18, 46	syl 10	. 2 |- (A.x e. X E.c e. RR A.n e. NN (N` ((T` n)` x)) <_ c -> E.k e. NN ((int` J)` (A` k)) =/= (/))
48	8	imsmet 8324	. . . . . . . . . . . 12 |- (U e. NrmCVec -> D e. Met)
49	31, 48	ax-mp 7	. . . . . . . . . . 11 |- D e. Met
50	9	opntop 7870	. . . . . . . . . . 11 |- (D e. Met -> J e. Top)
51	49, 50	ax-mp 7	. . . . . . . . . 10 |- J e. Top
52	37, 9	uniopn 7861	. . . . . . . . . . . . 13 |- (D e. Met -> U.J = X)
53	49, 52	ax-mp 7	. . . . . . . . . . . 12 |- U.J = X
54	53	eqcomi 1479	. . . . . . . . . . 11 |- X = U.J
55	54	ntrss2 7690	. . . . . . . . . 10 |- ((J e. Top /\ (A` k) (_ X) -> ((int` J)` (A` k)) (_ (A` k))
56	51, 55	mpan 695	. . . . . . . . 9 |- ((A` k) (_ X -> ((int` J)` (A` k)) (_ (A` k))
57	39, 56	syl 10	. . . . . . . 8 |- (k e. NN -> ((int` J)` (A` k)) (_ (A` k))
58	57, 39	sstrd 2074	. . . . . . 7 |- (k e. NN -> ((int` J)` (A` k)) (_ X)
59	58	sseld 2067	. . . . . 6 |- (k e. NN -> (p e. ((int` J)` (A` k)) -> p e. X))
60	9	opni2 7865	. . . . . . . . . 10 |- ((D e. Met /\ ((int` J)` (A` k)) e. J /\ p e. ((int` J)` (A` k))) -> E.r e. RR (0 < r /\ (p( ball ` D)r) (_ ((int` J)` (A` k))))
61	49, 60	mp3an1 903	. . . . . . . . 9 |- ((((int` J)` (A` k)) e. J /\ p e. ((int` J)` (A` k))) -> E.r e. RR (0 < r /\ (p( ball ` D)r) (_ ((int` J)` (A` k))))
62	54	ntropn 7684	. . . . . . . . . . 11 |- ((J e. Top /\ (A` k) (_ X) -> ((int` J)` (A` k)) e. J)
63	51, 62	mpan 695	. . . . . . . . . 10 |- ((A` k) (_ X -> ((int` J)` (A` k)) e. J)
64	39, 63	syl 10	. . . . . . . . 9 |- (k e. NN -> ((int` J)` (A` k)) e. J)
65	61, 64	sylan 448	. . . . . . . 8 |- ((k e. NN /\ p e. ((int` J)` (A` k))) -> E.r e. RR (0 < r /\ (p( ball ` D)r) (_ ((int` J)` (A` k))))
66	65	ex 373	. . . . . . 7 |- (k e. NN -> (p e. ((int` J)` (A` k)) -> E.r e. RR (0 < r /\ (p( ball ` D)r) (_ ((int` J)` (A` k)))))
67		sstr 2072	. . . . . . . . . . 11 |- (((p( ball ` D)r) (_ ((int` J)` (A` k)) /\ ((int` J)` (A` k)) (_ (A` k)) -> (p( ball ` D)r) (_ (A` k))
68	67, 57	sylan2 451	. . . . . . . . . 10 |- (((p( ball ` D)r) (_ ((int` J)` (A` k)) /\ k e. NN) -> (p( ball ` D)r) (_ (A` k))
69	68	expcom 374	. . . . . . . . 9 |- (k e. NN -> ((p( ball ` D)r) (_ ((int` J)` (A` k)) -> (p( ball ` D)r) (_ (A` k)))
70	69	anim2d 561	. . . . . . . 8 |- (k e. NN -> ((0 < r /\ (p( ball ` D)r) (_ ((int` J)` (A` k))) -> (0 < r /\ (p( ball ` D)r) (_ (A` k))))
71	70	r19.22sdv 1738	. . . . . . 7 |- (k e. NN -> (E.r e. RR (0 < r /\ (p( ball ` D)r) (_ ((int` J)` (A` k))) -> E.r e. RR (0 < r /\ (p( ball ` D)r) (_ (A` k))))
72	66, 71	syld 27	. . . . . 6 |- (k e. NN -> (p e. ((int` J)` (A` k)) -> E.r e. RR (0 < r /\ (p( ball ` D)r) (_ (A` k))))
73	59, 72	jcad 600	. . . . 5 |- (k e. NN -> (p e. ((int` J)` (A` k)) -> (p e. X /\ E.r e. RR (0 < r /\ (p( ball ` D)r) (_ (A` k)))))
74	73	19.22dv 1290	. . . 4 |- (k e. NN -> (E.p p e. ((int` J)` (A` k)) -> E.p(p e. X /\ E.r e. RR (0 < r /\ (p( ball ` D)r) (_ (A` k)))))
75		ne0 2288	. . . 4 |- (((int` J)` (A` k)) =/= (/) <-> E.p p e. ((int` J)` (A` k)))
76		df-rex 1650	. . . 4 |- (E.p e. X E.r e. RR (0 < r /\ (p( ball ` D)r) (_ <