Metamath Proof Explorer

Theorem istotbnd2

Description: The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	istotbnd2	\|- ( M e. ( Met ` X ) -> ( 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 ) ) ) )

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	baib	\|- ( M e. ( Met ` X ) -> ( 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 ) ) ) )

Step

Hyp

Ref

Expression

 |-  ( 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 ) ) ) )

 |-  ( M e. ( Met ` X ) -> ( 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 ) ) ) )