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 )