Theorem totbndss

Description: A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	totbndss	|- ( ( M e. ( TotBnd ` X ) /\ S C_ X ) -> ( M |` ( S X. S ) ) e. ( TotBnd ` S ) )

Proof

Step	Hyp	Ref	Expression
1		istotbnd	|- ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
2	1	simprbi	|- ( M e. ( TotBnd ` X ) -> A. d e. RR+ E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) )
3		sseq2	|- ( U. v = X -> ( S C_ U. v <-> S C_ X ) )
4	3	biimprcd	|- ( S C_ X -> ( U. v = X -> S C_ U. v ) )
5	4	anim1d	|- ( S C_ X -> ( ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> ( S C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
6	5	reximdv	|- ( S C_ X -> ( E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> E. v e. Fin ( S C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
7	6	ralimdv	|- ( S C_ X -> ( A. d e. RR+ E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) -> A. d e. RR+ E. v e. Fin ( S C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
8	2 7	mpan9	|- ( ( M e. ( TotBnd ` X ) /\ S C_ X ) -> A. d e. RR+ E. v e. Fin ( S C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) )
9		totbndmet	|- ( M e. ( TotBnd ` X ) -> M e. ( Met ` X ) )
10		eqid	|- ( M |` ( S X. S ) ) = ( M |` ( S X. S ) )
11	10	sstotbnd	|- ( ( M e. ( Met ` X ) /\ S C_ X ) -> ( ( M |` ( S X. S ) ) e. ( TotBnd ` S ) <-> A. d e. RR+ E. v e. Fin ( S C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
12	9 11	sylan	|- ( ( M e. ( TotBnd ` X ) /\ S C_ X ) -> ( ( M |` ( S X. S ) ) e. ( TotBnd ` S ) <-> A. d e. RR+ E. v e. Fin ( S C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
13	8 12	mpbird	|- ( ( M e. ( TotBnd ` X ) /\ S C_ X ) -> ( M |` ( S X. S ) ) e. ( TotBnd ` S ) )