Metamath Proof Explorer

Theorem 0totbnd

Description: The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion 0totbnd 
|- ( X = (/) -> ( M e. ( TotBnd ` X ) <-> M e. ( Met ` X ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( X = (/) -> ( TotBnd ` X ) = ( TotBnd ` (/) ) )
2 1 eleq2d 
 |-  ( X = (/) -> ( M e. ( TotBnd ` X ) <-> M e. ( TotBnd ` (/) ) ) )
3 0elpw 
 |-  (/) e. ~P (/)
4 0fin 
 |-  (/) e. Fin
5 elin 
 |-  ( (/) e. ( ~P (/) i^i Fin ) <-> ( (/) e. ~P (/) /\ (/) e. Fin ) )
6 3 4 5 mpbir2an 
 |-  (/) e. ( ~P (/) i^i Fin )
7 0iun 
 |-  U_ x e. (/) ( x ( ball ` M ) r ) = (/)
8 iuneq1 
 |-  ( v = (/) -> U_ x e. v ( x ( ball ` M ) r ) = U_ x e. (/) ( x ( ball ` M ) r ) )
9 8 eqeq1d 
 |-  ( v = (/) -> ( U_ x e. v ( x ( ball ` M ) r ) = (/) <-> U_ x e. (/) ( x ( ball ` M ) r ) = (/) ) )
10 9 rspcev 
 |-  ( ( (/) e. ( ~P (/) i^i Fin ) /\ U_ x e. (/) ( x ( ball ` M ) r ) = (/) ) -> E. v e. ( ~P (/) i^i Fin ) U_ x e. v ( x ( ball ` M ) r ) = (/) )
11 6 7 10 mp2an 
 |-  E. v e. ( ~P (/) i^i Fin ) U_ x e. v ( x ( ball ` M ) r ) = (/)
12 11 rgenw 
 |-  A. r e. RR+ E. v e. ( ~P (/) i^i Fin ) U_ x e. v ( x ( ball ` M ) r ) = (/)
13 istotbnd3 
 |-  ( M e. ( TotBnd ` (/) ) <-> ( M e. ( Met ` (/) ) /\ A. r e. RR+ E. v e. ( ~P (/) i^i Fin ) U_ x e. v ( x ( ball ` M ) r ) = (/) ) )
14 12 13 mpbiran2 
 |-  ( M e. ( TotBnd ` (/) ) <-> M e. ( Met ` (/) ) )
15 fveq2 
 |-  ( X = (/) -> ( Met ` X ) = ( Met ` (/) ) )
16 15 eleq2d 
 |-  ( X = (/) -> ( M e. ( Met ` X ) <-> M e. ( Met ` (/) ) ) )
17 14 16 bitr4id 
 |-  ( X = (/) -> ( M e. ( TotBnd ` (/) ) <-> M e. ( Met ` X ) ) )
18 2 17 bitrd 
 |-  ( X = (/) -> ( M e. ( TotBnd ` X ) <-> M e. ( Met ` X ) ) )