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∈∞Met⁡X→ran⁡ball⁡D∈TopBases

Proof

Step Hyp Ref Expression
1 blin2 ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→∃r∈ℝ+zball⁡Dr⊆x∩y
2 simpll ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→D∈∞Met⁡X
3 elinel1 ⊢z∈x∩y→z∈x
4 elunii ⊢z∈x∧x∈ran⁡ball⁡D→z∈⋃ran⁡ball⁡D
5 3 4 sylan ⊢z∈x∩y∧x∈ran⁡ball⁡D→z∈⋃ran⁡ball⁡D
6 5 ad2ant2lr ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→z∈⋃ran⁡ball⁡D
7 unirnbl ⊢D∈∞Met⁡X→⋃ran⁡ball⁡D=X
8 7 ad2antrr ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→⋃ran⁡ball⁡D=X
9 6 8 eleqtrd ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→z∈X
10 blssex ⊢D∈∞Met⁡X∧z∈X→∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y↔∃r∈ℝ+zball⁡Dr⊆x∩y
11 2 9 10 syl2anc ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y↔∃r∈ℝ+zball⁡Dr⊆x∩y
12 1 11 mpbird ⊢D∈∞Met⁡X∧z∈x∩y∧x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y
13 12 ex ⊢D∈∞Met⁡X∧z∈x∩y→x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y
14 13 ralrimdva ⊢D∈∞Met⁡X→x∈ran⁡ball⁡D∧y∈ran⁡ball⁡D→∀z∈x∩y∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y
15 14 ralrimivv ⊢D∈∞Met⁡X→∀x∈ran⁡ball⁡D∀y∈ran⁡ball⁡D∀z∈x∩y∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y
16 fvex ⊢ball⁡D∈V
17 16 rnex ⊢ran⁡ball⁡D∈V
18 isbasis2g ⊢ran⁡ball⁡D∈V→ran⁡ball⁡D∈TopBases↔∀x∈ran⁡ball⁡D∀y∈ran⁡ball⁡D∀z∈x∩y∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y
19 17 18 ax-mp ⊢ran⁡ball⁡D∈TopBases↔∀x∈ran⁡ball⁡D∀y∈ran⁡ball⁡D∀z∈x∩y∃b∈ran⁡ball⁡Dz∈b∧b⊆x∩y
20 15 19 sylibr ⊢D∈∞Met⁡X→ran⁡ball⁡D∈TopBases