Theorem ubthlem5 8533

Description: Lemma for ubthi 8544. The union of all A` k equals the base set, provided the values of the operators T` n are bounded for each vector x.

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
ubthlem5	|- (A.x e. X E.c e. RR A.n e. NN (N` ((T` n)` x)) <_ c -> U_k e. NN (A` k) = X)

Distinct variable groups:   k,c,n,x,A   D,k,n,x   k,J,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 ubthlem5

Step	Hyp	Ref	Expression
1		iunss 2591	. . . 4 |- (U_k e. NN (A` k) (_ X <-> A.k e. NN (A` k) (_ X)
2		ubthlem4.1	. . . . 5 |- X = (Base` U)
3		ubthlem4.11	. . . . 5 |- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
4	2, 3	ubthlem2 8530	. . . 4 |- (k e. NN -> (A` k) (_ X)
5	1, 4	mprgbir 1701	. . 3 |- U_k e. NN (A` k) (_ X
6	5	a1i 8	. 2 |- (A.x e. X E.c e. RR A.n e. NN (N` ((T` n)` x)) <_ c -> U_k e. NN (A` k) (_ X)
7		arch 6071	. . . . . . . . . . 11 |- (c e. RR -> E.k e. NN c < k)
8	7	ad2antlr 405	. . . . . . . . . 10 |- (((x e. X /\ c e. RR) /\ A.n e. NN (N` ((T` n)` x)) <_ c) -> E.k e. NN c < k)
9		ltlet 5520	. . . . . . . . . . . . . . 15 |- ((c e. RR /\ k e. RR) -> (c < k -> c <_ k))
10		nnret 5929	. . . . . . . . . . . . . . 15 |- (k e. NN -> k e. RR)
11	9, 10	sylan2 451	. . . . . . . . . . . . . 14 |- ((c e. RR /\ k e. NN) -> (c < k -> c <_ k))
12	11	adantll 392	. . . . . . . . . . . . 13 |- (((x e. X /\ c e. RR) /\ k e. NN) -> (c < k -> c <_ k))
13	12	adantlr 393	. . . . . . . . . . . 12 |- ((((x e. X /\ c e. RR) /\ A.n e. NN (N` ((T` n)` x)) <_ c) /\ k e. NN) -> (c < k -> c <_ k))
14		letrt 5525	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((N` ((T` n)` x)) e. RR /\ c e. RR /\ k e. RR) -> (((N` ((T` n)` x)) <_ c /\ c <_ k) -> (N` ((T` n)` x)) <_ k))
15		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((T` n):X-->Y /\ x e. X) -> ((T` n)` x) e. Y)
16		ubthlem4.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- T:NN-->B
17	16	ffvelrni 3815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (n e. NN -> (T` n) e. B)
18		ubthlem4.7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- U e. CBan
19		bnnv 8526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (U e. CBan -> U e. NrmCVec)
20	18, 19	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- U e. NrmCVec
21		ubthlem4.8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- W e. NrmCVec
22		ubthlem4.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- Y = (Base` W)
23		ubthlem4.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- B = (U BLnOp W)
24	2, 22, 23	blof 8445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((U e. NrmCVec /\ W e. NrmCVec /\ (T` n) e. B) -> (T` n):X-->Y)
25	20, 21, 24	mp3an12 906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((T` n) e. B -> (T` n):X-->Y)
26	17, 25	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (n e. NN -> (T` n):X-->Y)
27	15, 26	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((n e. NN /\ x e. X) -> ((T` n)` x) e. Y)
28	27	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. X /\ n e. NN) -> ((T` n)` x) e. Y)
29		ubthlem4.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- N = (norm` W)
30	22, 29	nvcl 8287	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((W e. NrmCVec /\ ((T` n)` x) e. Y) -> (N` ((T` n)` x)) e. RR)
31	21, 30	mpan 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((T` n)` x) e. Y -> (N` ((T` n)` x)) e. RR)
32	28, 31	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x e. X /\ n e. NN) -> (N` ((T` n)` x)) e. RR)
33	32	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x e. X /\ c e. RR) /\ n e. NN) -> (N` ((T` n)` x)) e. RR)
34	33	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ n e. NN) -> (N` ((T` n)` x)) e. RR)
35		simplr 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x e. X /\ c e. RR) /\ k e. NN) -> c e. RR)
36	35	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ n e. NN) -> c e. RR)
37	10	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ n e. NN) -> k e. RR)
38	14, 34, 36, 37	syl3anc 858	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ n e. NN) -> (((N` ((T` n)` x)) <_ c /\ c <_ k) -> (N` ((T` n)` x)) <_ k))
39	38	exp4b 379	. . . . . . . . . . . . . . . . . . . . . 22 |- (((x e. X /\ c e. RR) /\ k e. NN) -> (n e. NN -> ((N` ((T` n)` x)) <_ c -> (c <_ k -> (N` ((T` n)` x)) <_ k))))
40	39	com34 36	. . . . . . . . . . . . . . . . . . . . 21 |- (((x e. X /\ c e. RR) /\ k e. NN) -> (n e. NN -> (c <_ k -> ((N` ((T` n)` x)) <_ c -> (N` ((T` n)` x)) <_ k))))
41	40	com23 32	. . . . . . . . . . . . . . . . . . . 20 |- (((x e. X /\ c e. RR) /\ k e. NN) -> (c <_ k -> (n e. NN -> ((N` ((T` n)` x)) <_ c -> (N` ((T` n)` x)) <_ k))))
42	41	imp31 362	. . . . . . . . . . . . . . . . . . 19 |- (((((x e. X /\ c e. RR) /\ k e. NN) /\ c <_ k) /\ n e. NN) -> ((N` ((T` n)` x)) <_ c -> (N` ((T` n)` x)) <_ k))
43	42	r19.20dva 1709	. . . . . . . . . . . . . . . . . 18 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ c <_ k) -> (A.n e. NN (N` ((T` n)` x)) <_ c -> A.n e. NN (N` ((T` n)` x)) <_ k))
44	43	ex 373	. . . . . . . . . . . . . . . . 17 |- (((x e. X /\ c e. RR) /\ k e. NN) -> (c <_ k -> (A.n e. NN (N` ((T` n)` x)) <_ c -> A.n e. NN (N` ((T` n)` x)) <_ k)))
45	44	com23 32	. . . . . . . . . . . . . . . 16 |- (((x e. X /\ c e. RR) /\ k e. NN) -> (A.n e. NN (N` ((T` n)` x)) <_ c -> (c <_ k -> A.n e. NN (N` ((T` n)` x)) <_ k)))
46	45	imp 350	. . . . . . . . . . . . . . 15 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ A.n e. NN (N` ((T` n)` x)) <_ c) -> (c <_ k -> A.n e. NN (N` ((T` n)` x)) <_ k))
47		simpll 412	. . . . . . . . . . . . . . . 16 |- (((x e. X /\ c e. RR) /\ k e. NN) -> x e. X)
48	47	adantr 389	. . . . . . . . . . . . . . 15 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ A.n e. NN (N` ((T` n)` x)) <_ c) -> x e. X)
49	46, 48	jctild 601	. . . . . . . . . . . . . 14 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ A.n e. NN (N` ((T` n)` x)) <_ c) -> (c <_ k -> (x e. X /\ A.n e. NN (N` ((T` n)` x)) <_ k)))
50	2, 3	ubthlem1 8529	. . . . . . . . . . . . . . 15 |- (k e. NN -> (x e. (A` k) <-> (x e. X /\ A.n e. NN (N` ((T` n)` x)) <_ k)))
51	50	ad2antlr 405	. . . . . . . . . . . . . 14 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ A.n e. NN (N` ((T` n)` x)) <_ c) -> (x e. (A` k) <-> (x e. X /\ A.n e. NN (N` ((T` n)` x)) <_ k)))
52	49, 51	sylibrd 204	. . . . . . . . . . . . 13 |- ((((x e. X /\ c e. RR) /\ k e. NN) /\ A.n e. NN (N` ((T` n)` x)) <_ c) -> (c <_ k -> x e. (A` k)))
53	52	an1rs 489	. . . . . . . . . . . 12 |- ((((x e. X /\ c e. RR) /\ A.n e. NN (N` ((T` n)` x)) <_ c) /\ k e. NN) -> (c <_ k -> x e. (A` k)))
54	13, 53	syld 27	. . . . . . . . . . 11 |- ((((x e. X /\ c e. RR) /\ A.n e. NN (N` ((T` n)` x)) <_ c) /\ k