Theorem ssblex 7853

Description: A nested ball exists whose radius is less than any desired amount.

Hypothesis

Ref	Expression
ssblex.1	|- X = dom dom D

Assertion

Ref	Expression
ssblex	|- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) -> E.x e. RR (0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)))

Distinct variable groups:   x,D   x,P   x,R   x,S

Proof of Theorem ssblex

Step	Hyp	Ref	Expression
1		lelttrit 5634	. . . 4 |- ((R e. RR /\ S e. RR) -> (R <_ S \/ S < R))
2	1	ad2ant2r 411	. . 3 |- (((R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) -> (R <_ S \/ S < R))
3	2	3adant1 799	. 2 |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) -> (R <_ S \/ S < R))
4		breq2 2628	. . . . . 6 |- (x = (R / 2) -> (0 < x <-> 0 < (R / 2)))
5		breq1 2627	. . . . . 6 |- (x = (R / 2) -> (x < R <-> (R / 2) < R))
6		opreq2 3975	. . . . . . 7 |- (x = (R / 2) -> (P( ball ` D)x) = (P( ball ` D)(R / 2)))
7	6	sseq1d 2091	. . . . . 6 |- (x = (R / 2) -> ((P( ball ` D)x) (_ (P( ball ` D)S) <-> (P( ball ` D)(R / 2)) (_ (P( ball ` D)S)))
8	4, 5, 7	3anbi123d 895	. . . . 5 |- (x = (R / 2) -> ((0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)) <-> (0 < (R / 2) /\ (R / 2) < R /\ (P( ball ` D)(R / 2)) (_ (P( ball ` D)S))))
9	8	rcla4ev 1880	. . . 4 |- (((R / 2) e. RR /\ (0 < (R / 2) /\ (R / 2) < R /\ (P( ball ` D)(R / 2)) (_ (P( ball ` D)S))) -> E.x e. RR (0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)))
10		rehalfclt 6036	. . . . . 6 |- (R e. RR -> (R / 2) e. RR)
11	10	ad2antrr 406	. . . . 5 |- (((R e. RR /\ 0 < R) /\ R <_ S) -> (R / 2) e. RR)
12	11	3ad2antl2 812	. . . 4 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (R / 2) e. RR)
13		halfpos2t 6039	. . . . . . . 8 |- (R e. RR -> (0 < R <-> 0 < (R / 2)))
14	13	biimpa 418	. . . . . . 7 |- ((R e. RR /\ 0 < R) -> 0 < (R / 2))
15	14	adantr 391	. . . . . 6 |- (((R e. RR /\ 0 < R) /\ R <_ S) -> 0 < (R / 2))
16	15	3ad2antl2 812	. . . . 5 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> 0 < (R / 2))
17		halfpost 6038	. . . . . . . 8 |- (R e. RR -> (0 < R <-> (R / 2) < R))
18	17	biimpa 418	. . . . . . 7 |- ((R e. RR /\ 0 < R) -> (R / 2) < R)
19	18	adantr 391	. . . . . 6 |- (((R e. RR /\ 0 < R) /\ R <_ S) -> (R / 2) < R)
20	19	3ad2antl2 812	. . . . 5 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (R / 2) < R)
21	10	adantr 391	. . . . . . . . . . 11 |- ((R e. RR /\ 0 < R) -> (R / 2) e. RR)
22	21	ad2antrr 406	. . . . . . . . . 10 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> (R / 2) e. RR)
23		simpll 414	. . . . . . . . . . 11 |- (((R e. RR /\ 0 < R) /\ S e. RR) -> R e. RR)
24	23	adantr 391	. . . . . . . . . 10 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> R e. RR)
25		simplr 415	. . . . . . . . . 10 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> S e. RR)
26	18	ad2antrr 406	. . . . . . . . . 10 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> (R / 2) < R)
27		pm3.27 323	. . . . . . . . . 10 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> R <_ S)
28	22, 24, 25, 26, 27	ltletrd 5540	. . . . . . . . 9 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> (R / 2) < S)
29		ltlet 5532	. . . . . . . . . . . 12 |- (((R / 2) e. RR /\ S e. RR) -> ((R / 2) < S -> (R / 2) <_ S))
30	29, 10	sylan 450	. . . . . . . . . . 11 |- ((R e. RR /\ S e. RR) -> ((R / 2) < S -> (R / 2) <_ S))
31	30	adantlr 395	. . . . . . . . . 10 |- (((R e. RR /\ 0 < R) /\ S e. RR) -> ((R / 2) < S -> (R / 2) <_ S))
32	31	adantr 391	. . . . . . . . 9 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> ((R / 2) < S -> (R / 2) <_ S))
33	28, 32	mpd 26	. . . . . . . 8 |- ((((R e. RR /\ 0 < R) /\ S e. RR) /\ R <_ S) -> (R / 2) <_ S)
34	33	adantlrr 401	. . . . . . 7 |- ((((R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (R / 2) <_ S)
35	34	3adantl1 805	. . . . . 6 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (R / 2) <_ S)
36		ssblex.1	. . . . . . . 8 |- X = dom dom D
37	36	ssbl 7852	. . . . . . 7 |- ((((D e. Met /\ P e. X) /\ ((R / 2) e. RR /\ 0 < (R / 2)) /\ (S e. RR /\ 0 < S)) /\ (R / 2) <_ S) -> (P( ball ` D)(R / 2)) (_ (P( ball ` D)S))
38	21, 14	jca 288	. . . . . . 7 |- ((R e. RR /\ 0 < R) -> ((R / 2) e. RR /\ 0 < (R / 2)))
39	37, 38	syl3anl2 876	. . . . . 6 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ (R / 2) <_ S) -> (P( ball ` D)(R / 2)) (_ (P( ball ` D)S))
40	35, 39	syldan 469	. . . . 5 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (P( ball ` D)(R / 2)) (_ (P( ball ` D)S))
41	16, 20, 40	3jca 821	. . . 4 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (0 < (R / 2) /\ (R / 2) < R /\ (P( ball ` D)(R / 2)) (_ (P( ball ` D)S)))
42	9, 12, 41	sylanc 473	. . 3 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> E.x e. RR (0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)))
43		breq2 2628	. . . . . 6 |- (x = S -> (0 < x <-> 0 < S))
44		breq1 2627	. . . . . 6 |- (x = S -> (x < R <-> S < R))
45		opreq2 3975	. . . . . . 7 |- (x = S -> (P( ball ` D)x) = (P( ball ` D)S))
46	45	sseq1d 2091	. . . . . 6 |- (x = S -> ((P( ball ` D)x) (_ (P( ball ` D)S) <-> (P( ball ` D)S) (_ (P( ball ` D)S)))
47	43, 44, 46	3anbi123d 895	. . . . 5 |- (x = S -> ((0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)) <-> (0 < S /\ S < R /\ (P( ball ` D)S) (_ (P( ball ` D)S))))
48	47	rcla4ev 1880	. . . 4 |- ((S e. RR /\ (0 < S /\ S < R /\ (P( ball ` D)S) (_ (P( ball ` D)S))) -> E.x e. RR (0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)))
49		simpll 414	. . . . 5 |- (((S e. RR /\ 0 < S) /\ S < R) -> S e. RR)
50	49	3ad2antl3 813	. . . 4 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ S < R) -> S e. RR)
51		simplr 415	. . . . . 6 |- (((S e. RR /\ 0 < S) /\ S < R) -> 0 < S)
52	51	3ad2antl3 813	. . . . 5 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ S < R) -> 0 < S)
53		pm3.27 323	. . . . 5 |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (