HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem blss 7793
Description: Any point P in a ball B can be centered in another ball that is a subset of B.
Assertion
Ref Expression
blss |- ((D e. Met /\ B e. ran ( ball ` D) /\ P e. B) -> E.x e. RR (0 < x /\ (P( ball ` D)x) (_ B))
Distinct variable groups:   x,B   x,D   x,P
Proof of Theorem blss
StepHypRef Expression
1 eqid 1468 . . . 4 |- dom dom D = dom dom D
21blrn2 7782 . . 3 |- (D e. Met -> (B e. ran ( ball ` D) <-> E.z e. dom dom DE.w e. RR (0 < w /\ B = {v e. dom dom D | (zDv) < w})))
3 breq2 2613 . . . . . . . . 9 |- (x = (w - (zDP)) -> (0 < x <-> 0 < (w - (zDP))))
4 opreq2 3954 . . . . . . . . . 10 |- (x = (w - (zDP)) -> (P( ball ` D)x) = (P( ball ` D)(w - (zDP))))
54sseq1d 2078 . . . . . . . . 9 |- (x = (w - (zDP)) -> ((P( ball ` D)x) (_ B <-> (P( ball ` D)(w - (zDP))) (_ B))
63, 5anbi12d 626 . . . . . . . 8 |- (x = (w - (zDP)) -> ((0 < x /\ (P( ball ` D)x) (_ B) <-> (0 < (w - (zDP)) /\ (P( ball ` D)(w - (zDP))) (_ B)))
76rcla4ev 1868 . . . . . . 7 |- (((w - (zDP)) e. RR /\ (0 < (w - (zDP)) /\ (P( ball ` D)(w - (zDP))) (_ B)) -> E.x e. RR (0 < x /\ (P( ball ` D)x) (_ B))
8 resubclt 5410 . . . . . . . . . 10 |- ((w e. RR /\ (zDP) e. RR) -> (w - (zDP)) e. RR)
9 pm3.27 323 . . . . . . . . . . 11 |- ((z e. dom dom D /\ w e. RR) -> w e. RR)
109ad2antlr 405 . . . . . . . . . 10 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ P e. dom dom D) -> w e. RR)
111metcl 7750 . . . . . . . . . . . 12 |- ((D e. Met /\ z e. dom dom D /\ P e. dom dom D) -> (zDP) e. RR)
12113expa 831 . . . . . . . . . . 11 |- (((D e. Met /\ z e. dom dom D) /\ P e. dom dom D) -> (zDP) e. RR)
1312adantlrr 399 . . . . . . . . . 10 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ P e. dom dom D) -> (zDP) e. RR)
148, 10, 13sylanc 471 . . . . . . . . 9 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ P e. dom dom D) -> (w - (zDP)) e. RR)
1514adantrr 395 . . . . . . . 8 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> (w - (zDP)) e. RR)
16 eleq2 1527 . . . . . . . . . 10 |- (B = {v e. dom dom D | (zDv) < w} -> (P e. B <-> P e. {v e. dom dom D | (zDv) < w}))
17 opreq2 3954 . . . . . . . . . . . 12 |- (v = P -> (zDv) = (zDP))
1817breq1d 2619 . . . . . . . . . . 11 |- (v = P -> ((zDv) < w <-> (zDP) < w))
1918elrab 1896 . . . . . . . . . 10 |- (P e. {v e. dom dom D | (zDv) < w} <-> (P e. dom dom D /\ (zDP) < w))
2016, 19syl6bb 534 . . . . . . . . 9 |- (B = {v e. dom dom D | (zDv) < w} -> (P e. B <-> (P e. dom dom D /\ (zDP) < w)))
2120biimpa 416 . . . . . . . 8 |- ((B = {v e. dom dom D | (zDv) < w} /\ P e. B) -> (P e. dom dom D /\ (zDP) < w))
2215, 21sylan2 451 . . . . . . 7 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (B = {v e. dom dom D | (zDv) < w} /\ P e. B)) -> (w - (zDP)) e. RR)
23 posdift 5627 . . . . . . . . . . . 12 |- (((zDP) e. RR /\ w e. RR) -> ((zDP) < w <-> 0 < (w - (zDP))))
2423, 13, 10sylanc 471 . . . . . . . . . . 11 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ P e. dom dom D) -> ((zDP) < w <-> 0 < (w - (zDP))))
2524biimpa 416 . . . . . . . . . 10 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ P e. dom dom D) /\ (zDP) < w) -> 0 < (w - (zDP)))
2625anasss 440 . . . . . . . . 9 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> 0 < (w - (zDP)))
2726, 21sylan2 451 . . . . . . . 8 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (B = {v e. dom dom D | (zDv) < w} /\ P e. B)) -> 0 < (w - (zDP)))
281blssm 7790 . . . . . . . . . . . 12 |- (((D e. Met /\ P e. dom dom D) /\ ((w - (zDP)) e. RR /\ 0 < (w - (zDP)))) -> (P( ball ` D)(w - (zDP))) (_ dom dom D)
29 pm3.26 319 . . . . . . . . . . . . 13 |- ((D e. Met /\ (z e. dom dom D /\ w e. RR)) -> D e. Met)
30 pm3.26 319 . . . . . . . . . . . . 13 |- ((P e. dom dom D /\ (zDP) < w) -> P e. dom dom D)
3129, 30anim12i 333 . . . . . . . . . . . 12 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> (D e. Met /\ P e. dom dom D))
3215, 26jca 288 . . . . . . . . . . . 12 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> ((w - (zDP)) e. RR /\ 0 < (w - (zDP))))
3328, 31, 32sylanc 471 . . . . . . . . . . 11 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> (P( ball ` D)(w - (zDP))) (_ dom dom D)
341elbl 7778 . . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. dom dom D) /\ ((w - (zDP)) e. RR /\ 0 < (w - (zDP)))) -> (v e. (P( ball ` D)(w - (zDP))) <-> (v e. dom dom D /\ (PDv) < (w - (zDP)))))
3534, 31, 32sylanc 471 . . . . . . . . . . . . 13 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> (v e. (P( ball ` D)(w - (zDP))) <-> (v e. dom dom D /\ (PDv) < (w - (zDP)))))
361metcl 7750 . . . . . . . . . . . . . . . 16 |- ((D e. Met /\ z e. dom dom D /\ v e. dom dom D) -> (zDv) e. RR)
3729ad2antrr 404 . . . . . . . . . . . . . . . 16 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) /\ (v e. dom dom D /\ (PDv) < (w - (zDP)))) -> D e. Met)
38 pm3.26 319 . . . . . . . . . . . . . . . . . 18 |- ((z e. dom dom D /\ w e. RR) -> z e. dom dom D)
3938ad2antlr 405 . . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) -> z e. dom dom D)
4039adantr 389 . . . . . . . . . . . . . . . 16 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) /\ (v e. dom dom D /\ (PDv) < (w - (zDP)))) -> z e. dom dom D)
41 simprl 414 . . . . . . . . . . . . . . . 16 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) /\ (v e. dom dom D /\ (PDv) < (w - (zDP)))) -> v e. dom dom D)
4236, 37, 40, 41syl3anc 856 . . . . . . . . . . . . . . 15 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) /\ (v e. dom dom D /\ (PDv) < (w - (zDP)))) -> (zDv) e. RR)
43 axaddrcl 5244 . . . . . . . . . . . . . . . 16 |- (((zDP) e. RR /\ (PDv) e. RR) -> ((zDP) + (PDv)) e. RR)
4430ad2antlr 405 . . . . . . . . . . . . . . . . 17 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zDP) < w)) /\ (v e. dom dom D /\ (PDv) < (w - (zDP)))) -> P e. dom dom D)
4511, 37, 40, 44syl3anc 856 . . . . . . . . . . . . . . . 16 |- ((((D e. Met /\ (z e. dom dom D /\ w e. RR)) /\ (P e. dom dom D /\ (zD