Metamath Proof Explorer

Theorem met2ndc

Description: A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis methaus.1 
|- J = ( MetOpen ` D )
Assertion met2ndc 
|- ( D e. ( *Met ` X ) -> ( J e. 2ndc <-> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) )

Proof

Step Hyp Ref Expression
1 methaus.1 
 |-  J = ( MetOpen ` D )
2 eqid 
 |-  U. J = U. J
3 2 2ndcsep 
 |-  ( J e. 2ndc -> E. x e. ~P U. J ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = U. J ) )
4 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
5 4 pweqd 
 |-  ( D e. ( *Met ` X ) -> ~P X = ~P U. J )
6 4 eqeq2d 
 |-  ( D e. ( *Met ` X ) -> ( ( ( cls ` J ) ` x ) = X <-> ( ( cls ` J ) ` x ) = U. J ) )
7 6 anbi2d 
 |-  ( D e. ( *Met ` X ) -> ( ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) <-> ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = U. J ) ) )
8 5 7 rexeqbidv 
 |-  ( D e. ( *Met ` X ) -> ( E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) <-> E. x e. ~P U. J ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = U. J ) ) )
9 3 8 syl5ibr 
 |-  ( D e. ( *Met ` X ) -> ( J e. 2ndc -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) )
10 elpwi 
 |-  ( x e. ~P X -> x C_ X )
11 1 met2ndci 
 |-  ( ( D e. ( *Met ` X ) /\ ( x C_ X /\ x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) -> J e. 2ndc )
12 11 3exp2 
 |-  ( D e. ( *Met ` X ) -> ( x C_ X -> ( x ~<_ _om -> ( ( ( cls ` J ) ` x ) = X -> J e. 2ndc ) ) ) )
13 12 imp4a 
 |-  ( D e. ( *Met ` X ) -> ( x C_ X -> ( ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) -> J e. 2ndc ) ) )
14 10 13 syl5 
 |-  ( D e. ( *Met ` X ) -> ( x e. ~P X -> ( ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) -> J e. 2ndc ) ) )
15 14 rexlimdv 
 |-  ( D e. ( *Met ` X ) -> ( E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) -> J e. 2ndc ) )
16 9 15 impbid 
 |-  ( D e. ( *Met ` X ) -> ( J e. 2ndc <-> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) )