This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metnrm

Description: A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013) (Revised by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metnrm.j 
|- J = ( MetOpen ` D )
Assertion metnrm 
|- ( D e. ( *Met ` X ) -> J e. Nrm )

Proof

Step Hyp Ref Expression
1 metnrm.j 
 |-  J = ( MetOpen ` D )
2 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
3 eqid 
 |-  ( u e. X |-> inf ( ran ( v e. x |-> ( u D v ) ) , RR* , < ) ) = ( u e. X |-> inf ( ran ( v e. x |-> ( u D v ) ) , RR* , < ) )
4 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. ( Clsd ` J ) /\ y e. ( Clsd ` J ) ) /\ ( x i^i y ) = (/) ) -> D e. ( *Met ` X ) )
5 simp2l 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. ( Clsd ` J ) /\ y e. ( Clsd ` J ) ) /\ ( x i^i y ) = (/) ) -> x e. ( Clsd ` J ) )
6 simp2r 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. ( Clsd ` J ) /\ y e. ( Clsd ` J ) ) /\ ( x i^i y ) = (/) ) -> y e. ( Clsd ` J ) )
7 simp3 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. ( Clsd ` J ) /\ y e. ( Clsd ` J ) ) /\ ( x i^i y ) = (/) ) -> ( x i^i y ) = (/) )
8 eqid 
 |-  U_ s e. y ( s ( ball ` D ) ( if ( 1 <_ ( ( u e. X |-> inf ( ran ( v e. x |-> ( u D v ) ) , RR* , < ) ) ` s ) , 1 , ( ( u e. X |-> inf ( ran ( v e. x |-> ( u D v ) ) , RR* , < ) ) ` s ) ) / 2 ) ) = U_ s e. y ( s ( ball ` D ) ( if ( 1 <_ ( ( u e. X |-> inf ( ran ( v e. x |-> ( u D v ) ) , RR* , < ) ) ` s ) , 1 , ( ( u e. X |-> inf ( ran ( v e. x |-> ( u D v ) ) , RR* , < ) ) ` s ) ) / 2 ) )
9 eqid 
 |-  ( u e. X |-> inf ( ran ( v e. y |-> ( u D v ) ) , RR* , < ) ) = ( u e. X |-> inf ( ran ( v e. y |-> ( u D v ) ) , RR* , < ) )
10 eqid 
 |-  U_ t e. x ( t ( ball ` D ) ( if ( 1 <_ ( ( u e. X |-> inf ( ran ( v e. y |-> ( u D v ) ) , RR* , < ) ) ` t ) , 1 , ( ( u e. X |-> inf ( ran ( v e. y |-> ( u D v ) ) , RR* , < ) ) ` t ) ) / 2 ) ) = U_ t e. x ( t ( ball ` D ) ( if ( 1 <_ ( ( u e. X |-> inf ( ran ( v e. y |-> ( u D v ) ) , RR* , < ) ) ` t ) , 1 , ( ( u e. X |-> inf ( ran ( v e. y |-> ( u D v ) ) , RR* , < ) ) ` t ) ) / 2 ) )
11 3 1 4 5 6 7 8 9 10 metnrmlem3 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. ( Clsd ` J ) /\ y e. ( Clsd ` J ) ) /\ ( x i^i y ) = (/) ) -> E. z e. J E. w e. J ( x C_ z /\ y C_ w /\ ( z i^i w ) = (/) ) )
12 11 3expia 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. ( Clsd ` J ) /\ y e. ( Clsd ` J ) ) ) -> ( ( x i^i y ) = (/) -> E. z e. J E. w e. J ( x C_ z /\ y C_ w /\ ( z i^i w ) = (/) ) ) )
13 12 ralrimivva 
 |-  ( D e. ( *Met ` X ) -> A. x e. ( Clsd ` J ) A. y e. ( Clsd ` J ) ( ( x i^i y ) = (/) -> E. z e. J E. w e. J ( x C_ z /\ y C_ w /\ ( z i^i w ) = (/) ) ) )
14 isnrm3 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. x e. ( Clsd ` J ) A. y e. ( Clsd ` J ) ( ( x i^i y ) = (/) -> E. z e. J E. w e. J ( x C_ z /\ y C_ w /\ ( z i^i w ) = (/) ) ) ) )
15 2 13 14 sylanbrc 
 |-  ( D e. ( *Met ` X ) -> J e. Nrm )