Theorem bcthlem29 8010

Description: Lemma for bcth 8015. Therefore the union of all members of reference sequence M does not occupy the entire metric space X. Also, use metric space completeness (via bcthlem23 8004) to eliminate the limit point q from the antecedents.

Hypotheses

Ref	Expression
bcthlem29.1	|- D e. CMet
bcthlem29.3	|- X = dom dom D
bcthlem29.4	|- J = (Open` D)
bcthlem29.5	|- M:NN-->P~X
bcthlem29.6	|- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
bcthlem29.7	|- A = (X X. {x e. RR | 0 < x})
bcthlem29.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem29	|- ((((2nd` Q) < (1 / 2) /\ ((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1)))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) -> -. U.ran M = X)

Distinct variable groups:   g,j,k,p,y,z,A   g,r,x,D,j,k,p,y,z   g,F,k   g,J,j,p,r,x,y,z   g,M,j,p,r,x,y,z   O,p,r,z   Q,g   g,X,j,k,p,r,x,y,z

Proof of Theorem bcthlem29

Step	Hyp	Ref	Expression
1		fveq2 3721	. . . . . . 7 |- ((g` 1) = Q -> (2nd` (g` 1)) = (2nd` Q))
2	1	breq1d 2626	. . . . . 6 |- ((g` 1) = Q -> ((2nd` (g` 1)) < (1 / 2) <-> (2nd` Q) < (1 / 2)))
3		bcthlem29.1	. . . . . . . . 9 |- D e. CMet
4		bcthlem29.3	. . . . . . . . 9 |- X = dom dom D
5		bcthlem29.6	. . . . . . . . 9 |- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
6		bcthlem29.7	. . . . . . . . 9 |- A = (X X. {x e. RR | 0 < x})
7		bcthlem29.8	. . . . . . . . 9 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
8	3, 4, 5, 6, 7	bcthlem23 8004	. . . . . . . 8 |- ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> E.q e. X (1st o. g)(~~>m` D)q)
9	8	exp32 377	. . . . . . 7 |- (g:NN-->A -> ((2nd` (g` 1)) < (1 / 2) -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> E.q e. X (1st o. g)(~~>m` D)q)))
10	9	com12 11	. . . . . 6 |- ((2nd` (g` 1)) < (1 / 2) -> (g:NN-->A -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> E.q e. X (1st o. g)(~~>m` D)q)))
11	2, 10	syl6bir 215	. . . . 5 |- ((g` 1) = Q -> ((2nd` Q) < (1 / 2) -> (g:NN-->A -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> E.q e. X (1st o. g)(~~>m` D)q))))
12	11	com3l 34	. . . 4 |- ((2nd` Q) < (1 / 2) -> (g:NN-->A -> ((g` 1) = Q -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> E.q e. X (1st o. g)(~~>m` D)q))))
13	12	imp45 372	. . 3 |- (((2nd` Q) < (1 / 2) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) -> E.q e. X (1st o. g)(~~>m` D)q)
14	13	adantlr 393	. 2 |- ((((2nd` Q) < (1 / 2) /\ ((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1)))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) -> E.q e. X (1st o. g)(~~>m` D)q)
15		bcthlem29.4	. . . . . . . . . 10 |- J = (Open` D)
16		bcthlem29.5	. . . . . . . . . 10 |- M:NN-->P~X
17	3, 4, 15, 16, 5, 6, 7	bcthlem28 8009	. . . . . . . . 9 |- ((((q e. X /\ ((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1)))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) /\ (1st o. g)(~~>m` D)q) -> -. E.m e. NN q e. (M` m))
18	17	exp41 382	. . . . . . . 8 |- (q e. X -> (((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1))) -> ((g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> ((1st o. g)(~~>m` D)q -> -. E.m e. NN q e. (M` m)))))
19	18	imp4c 366	. . . . . . 7 |- (q e. X -> (((((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) /\ (1st o. g)(~~>m` D)q) -> -. E.m e. NN q e. (M` m)))
20		eleq2 1534	. . . . . . . . . 10 |- (U.ran M = X -> (q e. U.ran M <-> q e. X))
21	20	biimpar 417	. . . . . . . . 9 |- ((U.ran M = X /\ q e. X) -> q e. U.ran M)
22		ffun 3626	. . . . . . . . . . . 12 |- (M:NN-->P~X -> Fun M)
23	16, 22	ax-mp 7	. . . . . . . . . . 11 |- Fun M
24		elunirn 3865	. . . . . . . . . . 11 |- (Fun M -> (q e. U.ran M <-> E.m e. dom M q e. (M` m)))
25	23, 24	ax-mp 7	. . . . . . . . . 10 |- (q e. U.ran M <-> E.m e. dom M q e. (M` m))
26		fdm 3628	. . . . . . . . . . . 12 |- (M:NN-->P~X -> dom M = NN)
27	16, 26	ax-mp 7	. . . . . . . . . . 11 |- dom M = NN
28		rexeq1 1786	. . . . . . . . . . 11 |- (dom M = NN -> (E.m e. dom M q e. (M` m) <-> E.m e. NN q e. (M` m)))
29	27, 28	ax-mp 7	. . . . . . . . . 10 |- (E.m e. dom M q e. (M` m) <-> E.m e. NN q e. (M` m))
30	25, 29	bitr 173	. . . . . . . . 9 |- (q e. U.ran M <-> E.m e. NN q e. (M` m))
31	21, 30	sylib 198	. . . . . . . 8 |- ((U.ran M = X /\ q e. X) -> E.m e. NN q e. (M` m))
32	31	expcom 374	. . . . . . 7 |- (q e. X -> (U.ran M = X -> E.m e. NN q e. (M` m)))
33	19, 32	nsyld 117	. . . . . 6 |- (q e. X -> (((((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) /\ (1st o. g)(~~>m` D)q) -> -. U.ran M = X))
34	33	exp3a 375	. . . . 5 |- (q e. X -> ((((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) -> ((1st o. g)(~~>m` D)q -> -. U.ran M = X)))
35	34	com12 11	. . . 4 |- ((((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) -> (q e. X -> ((1st o. g)(~~>m` D)q -> -. U.ran M = X)))
36	35	r19.23adv 1745	. . 3 |- ((((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1))) /\ (g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. (