Metamath Proof Explorer

Theorem blbnd

Description: A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 15-Jan-2014)

Ref Expression
Assertion blbnd 
|- ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> M e. ( *Met ` X ) )
2 rexr 
 |-  ( R e. RR -> R e. RR* )
3 blssm 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR* ) -> ( Y ( ball ` M ) R ) C_ X )
4 2 3 syl3an3 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> ( Y ( ball ` M ) R ) C_ X )
5 xmetres2 
 |-  ( ( M e. ( *Met ` X ) /\ ( Y ( ball ` M ) R ) C_ X ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( *Met ` ( Y ( ball ` M ) R ) ) )
6 1 4 5 syl2anc 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( *Met ` ( Y ( ball ` M ) R ) ) )
7 6 adantr 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) = (/) ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( *Met ` ( Y ( ball ` M ) R ) ) )
8 rzal 
 |-  ( ( Y ( ball ` M ) R ) = (/) -> A. x e. ( Y ( ball ` M ) R ) E. r e. RR+ ( Y ( ball ` M ) R ) = ( x ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) r ) )
9 8 adantl 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) = (/) ) -> A. x e. ( Y ( ball ` M ) R ) E. r e. RR+ ( Y ( ball ` M ) R ) = ( x ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) r ) )
10 isbndx 
 |-  ( ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) <-> ( ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( *Met ` ( Y ( ball ` M ) R ) ) /\ A. x e. ( Y ( ball ` M ) R ) E. r e. RR+ ( Y ( ball ` M ) R ) = ( x ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) r ) ) )
11 7 9 10 sylanbrc 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) = (/) ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) )
12 6 adantr 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( *Met ` ( Y ( ball ` M ) R ) ) )
13 1 adantr 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> M e. ( *Met ` X ) )
14 simpl2 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> Y e. X )
15 simpl3 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> R e. RR )
16 xbln0 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR* ) -> ( ( Y ( ball ` M ) R ) =/= (/) <-> 0 < R ) )
17 2 16 syl3an3 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> ( ( Y ( ball ` M ) R ) =/= (/) <-> 0 < R ) )
18 17 biimpa 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> 0 < R )
19 15 18 elrpd 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> R e. RR+ )
20 blcntr 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR+ ) -> Y e. ( Y ( ball ` M ) R ) )
21 13 14 19 20 syl3anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> Y e. ( Y ( ball ` M ) R ) )
22 14 21 elind 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> Y e. ( X i^i ( Y ( ball ` M ) R ) ) )
23 15 rexrd 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> R e. RR* )
24 eqid 
 |-  ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) = ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) )
25 24 blres 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. ( X i^i ( Y ( ball ` M ) R ) ) /\ R e. RR* ) -> ( Y ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) R ) = ( ( Y ( ball ` M ) R ) i^i ( Y ( ball ` M ) R ) ) )
26 13 22 23 25 syl3anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> ( Y ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) R ) = ( ( Y ( ball ` M ) R ) i^i ( Y ( ball ` M ) R ) ) )
27 inidm 
 |-  ( ( Y ( ball ` M ) R ) i^i ( Y ( ball ` M ) R ) ) = ( Y ( ball ` M ) R )
28 26 27 eqtr2di 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> ( Y ( ball ` M ) R ) = ( Y ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) R ) )
29 rspceov 
 |-  ( ( Y e. ( Y ( ball ` M ) R ) /\ R e. RR+ /\ ( Y ( ball ` M ) R ) = ( Y ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) R ) ) -> E. x e. ( Y ( ball ` M ) R ) E. r e. RR+ ( Y ( ball ` M ) R ) = ( x ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) r ) )
30 21 19 28 29 syl3anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> E. x e. ( Y ( ball ` M ) R ) E. r e. RR+ ( Y ( ball ` M ) R ) = ( x ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) r ) )
31 isbnd2 
 |-  ( ( ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) /\ ( Y ( ball ` M ) R ) =/= (/) ) <-> ( ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( *Met ` ( Y ( ball ` M ) R ) ) /\ E. x e. ( Y ( ball ` M ) R ) E. r e. RR+ ( Y ( ball ` M ) R ) = ( x ( ball ` ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) ) r ) ) )
32 12 30 31 sylanbrc 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> ( ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) /\ ( Y ( ball ` M ) R ) =/= (/) ) )
33 32 simpld 
 |-  ( ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) /\ ( Y ( ball ` M ) R ) =/= (/) ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) )
34 11 33 pm2.61dane 
 |-  ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) )