Theorem bcthlem33 8031

Description: Lemma for bcth 8032. All members of reference sequence M cannot have an empty interior.

Hypotheses

Ref	Expression
bcthlem34.1	|- D e. CMet
bcthlem34.2	|- X =/= (/)
bcthlem34.3	|- X = dom dom D
bcthlem34.4	|- J = (Open` D)
bcthlem34.5	|- M:NN-->P~X

Assertion

Ref	Expression
bcthlem33	|- ((U.ran M = X /\ ran M (_ (Clsd` J)) -> E.k e. NN ((int` J)` (M` k)) =/= (/))

Distinct variable groups:   D,k   k,J   k,M   k,X

Proof of Theorem bcthlem33

Step	Hyp	Ref	Expression
1		1nn 5934	. . . . . . . 8 |- 1 e. NN
2		fveq2 3724	. . . . . . . . . . . 12 |- (k = 1 -> (M` k) = (M` 1))
3	2	fveq2d 3728	. . . . . . . . . . 11 |- (k = 1 -> ((cls` J)` (M` k)) = ((cls` J)` (M` 1)))
4	3	fveq2d 3728	. . . . . . . . . 10 |- (k = 1 -> ((int` J)` ((cls` J)` (M` k))) = ((int` J)` ((cls` J)` (M` 1))))
5	4	eqeq1d 1483	. . . . . . . . 9 |- (k = 1 -> (((int` J)` ((cls` J)` (M` k))) = (/) <-> ((int` J)` ((cls` J)` (M` 1))) = (/)))
6	5	rcla4v 1873	. . . . . . . 8 |- (1 e. NN -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> ((int` J)` ((cls` J)` (M` 1))) = (/)))
7	1, 6	ax-mp 7	. . . . . . 7 |- (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> ((int` J)` ((cls` J)` (M` 1))) = (/))
8		bcthlem34.5	. . . . . . . . . . 11 |- M:NN-->P~X
9	8	ffvelrni 3815	. . . . . . . . . 10 |- (1 e. NN -> (M` 1) e. P~X)
10	1, 9	ax-mp 7	. . . . . . . . 9 |- (M` 1) e. P~X
11		elpwi 2406	. . . . . . . . 9 |- ((M` 1) e. P~X -> (M` 1) (_ X)
12	10, 11	ax-mp 7	. . . . . . . 8 |- (M` 1) (_ X
13		bcthlem34.1	. . . . . . . . 9 |- D e. CMet
14		bcthlem34.3	. . . . . . . . 9 |- X = dom dom D
15		bcthlem34.4	. . . . . . . . 9 |- J = (Open` D)
16		bcthlem34.2	. . . . . . . . 9 |- X =/= (/)
17	13, 14, 15, 16	bcthlem10 8008	. . . . . . . 8 |- (((M` 1) (_ X /\ ((int` J)` ((cls` J)` (M` 1))) = (/)) -> ((X \ ((cls` J)` (M` 1))) =/= (/) /\ (X \ ((cls` J)` (M` 1))) e. J))
18	12, 17	mpan 695	. . . . . . 7 |- (((int` J)` ((cls` J)` (M` 1))) = (/) -> ((X \ ((cls` J)` (M` 1))) =/= (/) /\ (X \ ((cls` J)` (M` 1))) e. J))
19	13, 14, 15	bcthlem8 8006	. . . . . . . 8 |- (((X \ ((cls` J)` (M` 1))) =/= (/) /\ (X \ ((cls` J)` (M` 1))) e. J /\ 1 e. NN) -> E.q e. (X \ ((cls` J)` (M` 1)))E.s e. RR (0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))))
20	1, 19	mp3an3 905	. . . . . . 7 |- (((X \ ((cls` J)` (M` 1))) =/= (/) /\ (X \ ((cls` J)` (M` 1))) e. J) -> E.q e. (X \ ((cls` J)` (M` 1)))E.s e. RR (0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))))
21	7, 18, 20	3syl 20	. . . . . 6 |- (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> E.q e. (X \ ((cls` J)` (M` 1)))E.s e. RR (0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))))
22	13, 14, 15, 8	bcthlem32 8030	. . . . . . . . . . . . . . . 16 |- (((s < (1 / 2) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))) /\ (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) /\ (q e. X /\ (s e. RR /\ 0 < s)))) -> -. U.ran M = X)
23	22	exp43 384	. . . . . . . . . . . . . . 15 |- (s < (1 / 2) -> ((q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1))) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> ((q e. X /\ (s e. RR /\ 0 < s)) -> -. U.ran M = X))))
24	23	com4r 41	. . . . . . . . . . . . . 14 |- ((q e. X /\ (s e. RR /\ 0 < s)) -> (s < (1 / 2) -> ((q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1))) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X))))
25	24	exp32 377	. . . . . . . . . . . . 13 |- (q e. X -> (s e. RR -> (0 < s -> (s < (1 / 2) -> ((q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1))) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X))))))
26	25	imp 350	. . . . . . . . . . . 12 |- ((q e. X /\ s e. RR) -> (0 < s -> (s < (1 / 2) -> ((q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1))) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X)))))
27	26	com4l 39	. . . . . . . . . . 11 |- (0 < s -> (s < (1 / 2) -> ((q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1))) -> ((q e. X /\ s e. RR) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X)))))
28		2cn 5980	. . . . . . . . . . . . . 14 |- 2 e. CC
29		exp1t 6573	. . . . . . . . . . . . . 14 |- (2 e. CC -> (2^1) = 2)
30	28, 29	ax-mp 7	. . . . . . . . . . . . 13 |- (2^1) = 2
31	30	opreq2i 3972	. . . . . . . . . . . 12 |- (1 / (2^1)) = (1 / 2)
32	31	breq2i 2627	. . . . . . . . . . 11 |- (s < (1 / (2^1)) <-> s < (1 / 2))
33	27, 32	syl5ib 206	. . . . . . . . . 10 |- (0 < s -> (s < (1 / (2^1)) -> ((q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1))) -> ((q e. X /\ s e. RR) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X)))))
34	33	3imp 827	. . . . . . . . 9 |- ((0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))) -> ((q e. X /\ s e. RR) -> (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X)))
35	34	com13 33	. . . . . . . 8 |- (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> ((q e. X /\ s e. RR) -> ((0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))) -> -. U.ran M = X)))
36		eldifi 2162	. . . . . . . 8 |- (q e. (X \ ((cls` J)` (M` 1))) -> q e. X)
37	35, 36	sylani 464	. . . . . . 7 |- (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> ((q e. (X \ ((cls` J)` (M` 1))) /\ s e. RR) -> ((0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))) -> -. U.ran M = X)))
38	37	r19.23advv 1749	. . . . . 6 |- (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> (E.q e. (X \ ((cls` J)` (M` 1)))E.s e. RR (0 < s /\ s < (1 / (2^1)) /\ (q( ball ` D)s) (_ (X \ ((cls` J)` (M` 1)))) -> -. U.ran M = X))
39	21, 38	mpd 26	. . . . 5 |- (A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/) -> -. U.ran M = X)
40	39	con2i 97	. . . 4 |- (U.ran M = X -> -. A.k e. NN ((int` J)` ((cls` J)` (M` k))) = (/))
41	40	adantr 389	. . 3 |- ((U.ran M = X /\ ran M (_ (Clsd` J)) -> -. A.k e. NN ((int` J