Theorem bcthlem14 8012

Description: Lemma for bcth 8032. Helper lemma for satisfying the antecendent of acdc5 7493.

Hypotheses

Ref	Expression
bcthlem15.1	|- D e. CMet
bcthlem15.3	|- X = dom dom D
bcthlem15.4	|- J = (Open` D)
bcthlem15.7	|- A = (X X. {x e. RR | 0 < x})
bcthlem15.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem14	|- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))} =/= (/))

Distinct variable groups:   j,p,y,A   x,r,D   x,p,J   M,p,x   r,p,O   j,r,x,X,p,y

Proof of Theorem bcthlem14

Step	Hyp	Ref	Expression
1		bcthlem15.1	. . . . . . 7 |- D e. CMet
2		bcthlem15.3	. . . . . . 7 |- X = dom dom D
3		bcthlem15.4	. . . . . . 7 |- J = (Open` D)
4		bcthlem15.8	. . . . . . 7 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
5	1, 2, 3, 4	bcthlem9 8007	. . . . . 6 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ ((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y))) -> (O =/= (/) /\ O e. J))
6		bcthlem15.7	. . . . . . . . 9 |- A = (X X. {x e. RR | 0 < x})
7	6	eleq2i 1538	. . . . . . . 8 |- (y e. A <-> y e. (X X. {x e. RR | 0 < x}))
8		elxp6 4102	. . . . . . . . . 10 |- (y e. (X X. {x e. RR | 0 < x}) <-> (y = <.(1st` y), (2nd` y)>. /\ ((1st` y) e. X /\ (2nd` y) e. {x e. RR | 0 < x})))
9	8	pm3.27bi 326	. . . . . . . . 9 |- (y e. (X X. {x e. RR | 0 < x}) -> ((1st` y) e. X /\ (2nd` y) e. {x e. RR | 0 < x}))
10		breq2 2623	. . . . . . . . . . . 12 |- (x = (2nd` y) -> (0 < x <-> 0 < (2nd` y)))
11	10	elrab 1905	. . . . . . . . . . 11 |- ((2nd` y) e. {x e. RR | 0 < x} <-> ((2nd` y) e. RR /\ 0 < (2nd` y)))
12	11	anbi2i 480	. . . . . . . . . 10 |- (((1st` y) e. X /\ (2nd` y) e. {x e. RR | 0 < x}) <-> ((1st` y) e. X /\ ((2nd` y) e. RR /\ 0 < (2nd` y))))
13		3anass 779	. . . . . . . . . 10 |- (((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y)) <-> ((1st` y) e. X /\ ((2nd` y) e. RR /\ 0 < (2nd` y))))
14	12, 13	bitr4 176	. . . . . . . . 9 |- (((1st` y) e. X /\ (2nd` y) e. {x e. RR | 0 < x}) <-> ((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y)))
15	9, 14	sylib 198	. . . . . . . 8 |- (y e. (X X. {x e. RR | 0 < x}) -> ((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y)))
16	7, 15	sylbi 199	. . . . . . 7 |- (y e. A -> ((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y)))
17	16	adantl 388	. . . . . 6 |- ((j e. NN /\ y e. A) -> ((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y)))
18	5, 17	sylan2 451	. . . . 5 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> (O =/= (/) /\ O e. J))
19	18	pm3.26d 321	. . . 4 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> O =/= (/))
20		ne0 2288	. . . 4 |- (O =/= (/) <-> E.p p e. O)
21	19, 20	sylib 198	. . 3 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> E.p p e. O)
22		inss1 2230	. . . . . . . . . 10 |- ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))) (_ (X \ ((cls` J)` (M` j)))
23		difss 2167	. . . . . . . . . 10 |- (X \ ((cls` J)` (M` j))) (_ X
24	22, 23	sstri 2073	. . . . . . . . 9 |- ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2))) (_ X
25	4, 24	eqsstr 2091	. . . . . . . 8 |- O (_ X
26	25	sseli 2065	. . . . . . 7 |- (p e. O -> p e. X)
27	26	a1i 8	. . . . . 6 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> (p e. O -> p e. X))
28	1	cmsmeti 7962	. . . . . . . . . 10 |- D e. Met
29	3	opni3 7866	. . . . . . . . . 10 |- (((D e. Met /\ O e. J /\ p e. O) /\ (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2))) -> E.r e. RR (0 < r /\ r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))
30	28, 29	mp3anl1 910	. . . . . . . . 9 |- (((O e. J /\ p e. O) /\ (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2))) -> E.r e. RR (0 < r /\ r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))
31	18	pm3.27d 325	. . . . . . . . . 10 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> O e. J)
32	31	anim1i 334	. . . . . . . . 9 |- (((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) /\ p e. O) -> (O e. J /\ p e. O))
33		rehalfclt 6034	. . . . . . . . . . . . . . 15 |- ((2nd` y) e. RR -> ((2nd` y) / 2) e. RR)
34	33	adantr 389	. . . . . . . . . . . . . 14 |- (((2nd` y) e. RR /\ 0 < (2nd` y)) -> ((2nd` y) / 2) e. RR)
35		halfpos2t 6037	. . . . . . . . . . . . . . 15 |- ((2nd` y) e. RR -> (0 < (2nd` y) <-> 0 < ((2nd` y) / 2)))
36	35	biimpa 416	. . . . . . . . . . . . . 14 |- (((2nd` y) e. RR /\ 0 < (2nd` y)) -> 0 < ((2nd` y) / 2))
37	34, 36	jca 288	. . . . . . . . . . . . 13 |- (((2nd` y) e. RR /\ 0 < (2nd` y)) -> (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2)))
38	37	3adant1 797	. . . . . . . . . . . 12 |- (((1st` y) e. X /\ (2nd` y) e. RR /\ 0 < (2nd` y)) -> (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2)))
39	16, 38	syl 10	. . . . . . . . . . 11 |- (y e. A -> (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2)))
40	39	adantl 388	. . . . . . . . . 10 |- ((j e. NN /\ y e. A) -> (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2)))
41	40	ad2antlr 405	. . . . . . . . 9 |- (((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) /\ p e. O) -> (((2nd` y) / 2) e. RR /\ 0 < ((2nd` y) / 2)))
42	30, 32, 41	sylanc 471	. . . . . . . 8 |- (((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) /\ p e. O) -> E.r e. RR (0 < r /\ r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))
43	42	ex 373	. . . . . . 7 |- ((((M` j) (_ X /\ ((int` J)` ((cls` J)` (M` j))) = (/)) /\ (j e. NN /\ y e. A)) -> (p e. O -> E.r e. RR (0 < r /\ r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O)))
44		df-rex 1650	. . . . . . . 8 |- (E.r e. RR (0 < r /\ r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O) <-> E.r(r e. RR /\ (0 < r /\ r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O)))
45		anass 439	. . . . . . . . . 10 |- (((r e. RR /\ 0 < r) /\ (r < ((2nd` y) / 2)