Metamath Proof Explorer

Theorem blbas

Description: The balls of a metric space form a basis for a topology. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 15-Jan-2014)

Ref Expression
Assertion blbas 
|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) e. TopBases )

Proof

Step Hyp Ref Expression
1 blin2 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> E. r e. RR+ ( z ( ball ` D ) r ) C_ ( x i^i y ) )
2 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> D e. ( *Met ` X ) )
3 elinel1 
 |-  ( z e. ( x i^i y ) -> z e. x )
4 elunii 
 |-  ( ( z e. x /\ x e. ran ( ball ` D ) ) -> z e. U. ran ( ball ` D ) )
5 3 4 sylan 
 |-  ( ( z e. ( x i^i y ) /\ x e. ran ( ball ` D ) ) -> z e. U. ran ( ball ` D ) )
6 5 ad2ant2lr 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> z e. U. ran ( ball ` D ) )
7 unirnbl 
 |-  ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X )
8 7 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> U. ran ( ball ` D ) = X )
9 6 8 eleqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> z e. X )
10 blssex 
 |-  ( ( D e. ( *Met ` X ) /\ z e. X ) -> ( E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) <-> E. r e. RR+ ( z ( ball ` D ) r ) C_ ( x i^i y ) ) )
11 2 9 10 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> ( E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) <-> E. r e. RR+ ( z ( ball ` D ) r ) C_ ( x i^i y ) ) )
12 1 11 mpbird 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) /\ ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) ) -> E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) )
13 12 ex 
 |-  ( ( D e. ( *Met ` X ) /\ z e. ( x i^i y ) ) -> ( ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) -> E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) )
14 13 ralrimdva 
 |-  ( D e. ( *Met ` X ) -> ( ( x e. ran ( ball ` D ) /\ y e. ran ( ball ` D ) ) -> A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) )
15 14 ralrimivv 
 |-  ( D e. ( *Met ` X ) -> A. x e. ran ( ball ` D ) A. y e. ran ( ball ` D ) A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) )
16 fvex 
 |-  ( ball ` D ) e. _V
17 16 rnex 
 |-  ran ( ball ` D ) e. _V
18 isbasis2g 
 |-  ( ran ( ball ` D ) e. _V -> ( ran ( ball ` D ) e. TopBases <-> A. x e. ran ( ball ` D ) A. y e. ran ( ball ` D ) A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) ) )
19 17 18 ax-mp 
 |-  ( ran ( ball ` D ) e. TopBases <-> A. x e. ran ( ball ` D ) A. y e. ran ( ball ` D ) A. z e. ( x i^i y ) E. b e. ran ( ball ` D ) ( z e. b /\ b C_ ( x i^i y ) ) )
20 15 19 sylibr 
 |-  ( D e. ( *Met ` X ) -> ran ( ball ` D ) e. TopBases )