Theorem bcthlem28 8023

Description: Lemma for bcth 8029. The convergence point q does not belong to any member of reference sequence M.

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
bcthlem28	|- ((((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))

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

Proof of Theorem bcthlem28

Step	Hyp	Ref	Expression
1		fveq2 3730	. . . . . . . . . . . . . 14 |- ((g` 1) = Q -> (1st` (g` 1)) = (1st` Q))
2		fveq2 3730	. . . . . . . . . . . . . 14 |- ((g` 1) = Q -> (2nd` (g` 1)) = (2nd` Q))
3	1, 2	opreq12d 3984	. . . . . . . . . . . . 13 |- ((g` 1) = Q -> ((1st` (g` 1))( ball ` D)(2nd` (g` 1))) = ((1st` Q)( ball ` D)(2nd` Q)))
4	3	sseq1d 2091	. . . . . . . . . . . 12 |- ((g` 1) = Q -> (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) <-> ((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1)))))
5	4	adantr 391	. . . . . . . . . . 11 |- (((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) -> (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) <-> ((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1)))))
6	5	ad2antlr 407	. . . . . . . . . 10 |- (((g:NN-->A /\ ((g` 1) = Q /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN) -> (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) <-> ((1st` Q)( ball ` D)(2nd` Q)) (_ (X \ ((cls` J)` (M` 1)))))
7		bcthlem29.1	. . . . . . . . . . . . . . . . . . 19 |- D e. CMet
8		bcthlem29.3	. . . . . . . . . . . . . . . . . . 19 |- X = dom dom D
9		bcthlem29.6	. . . . . . . . . . . . . . . . . . 19 |- 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))})}
10		bcthlem29.7	. . . . . . . . . . . . . . . . . . 19 |- A = (X X. {x e. RR | 0 < x})
11		bcthlem29.8	. . . . . . . . . . . . . . . . . . 19 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
12	7, 8, 9, 10, 11	bcthlem27 8022	. . . . . . . . . . . . . . . . . 18 |- (((q e. X /\ ((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN)) /\ (1st o. g)(~~>m` D)q) -> q e. (X \ ((cls` J)` (M` m))))
13		bcthlem29.5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- M:NN-->P~X
14	13	ffvelrni 3821	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (m e. NN -> (M` m) e. P~X)
15		elpwi 2410	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((M` m) e. P~X -> (M` m) (_ X)
16	14, 15	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m e. NN -> (M` m) (_ X)
17		bcthlem29.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- J = (Open` D)
18	7, 8, 17	bcthlem6 8001	. . . . . . . . . . . . . . . . . . . . . . . 24 |- J e. Top
19	7, 8, 17	bcthlem5 8000	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- X = U.J
20	19	sscls 7686	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ (M` m) (_ X) -> (M` m) (_ ((cls` J)` (M` m)))
21	18, 20	mpan 697	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((M` m) (_ X -> (M` m) (_ ((cls` J)` (M` m)))
22	16, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- (m e. NN -> (M` m) (_ ((cls` J)` (M` m)))
23	22	sseld 2070	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. NN -> (q e. (M` m) -> q e. ((cls` J)` (M` m))))
24		eldifn 2166	. . . . . . . . . . . . . . . . . . . . 21 |- (q e. (X \ ((cls` J)` (M` m))) -> -. q e. ((cls` J)` (M` m)))
25	23, 24	nsyli 121	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> (q e. (X \ ((cls` J)` (M` m))) -> -. q e. (M` m)))
26	25	adantl 390	. . . . . . . . . . . . . . . . . . 19 |- (((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN) -> (q e. (X \ ((cls` J)` (M` m))) -> -. q e. (M` m)))
27	26	ad2antlr 407	. . . . . . . . . . . . . . . . . 18 |- (((q e. X /\ ((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN)) /\ (1st o. g)(~~>m` D)q) -> (q e. (X \ ((cls` J)` (M` m))) -> -. q e. (M` m)))
28	12, 27	mpd 26	. . . . . . . . . . . . . . . . 17 |- (((q e. X /\ ((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN)) /\ (1st o. g)(~~>m` D)q) -> -. q e. (M` m))
29	28	exp42 385	. . . . . . . . . . . . . . . 16 |- (q e. X -> ((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (m e. NN -> ((1st o. g)(~~>m` D)q -> -. q e. (M` m)))))
30	29	com3l 34	. . . . . . . . . . . . . . 15 |- ((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (m e. NN -> (q e. X -> ((1st o. g)(~~>m` D)q -> -. q e. (M` m)))))
31	30	exp32 379	. . . . . . . . . . . . . 14 |- (g:NN-->A -> (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> (m e. NN -> (q e. X -> ((1st o. g)(~~>m` D)q -> -. q e. (M` m)))))))
32	31	com23 32	. . . . . . . . . . . . 13 |- (g:NN-->A -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) -> (m e.