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 ∈ ℝ + z ball ⁡ D r ⊆ 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 ⁡ D z ∈ b ∧ b ⊆ x ∩ y ↔ ∃ r ∈ ℝ + z ball ⁡ D r ⊆ x ∩ y
11 2 9 10 syl2anc ⊢ D ∈ ∞Met ⁡ X ∧ z ∈ x ∩ y ∧ x ∈ ran ⁡ ball ⁡ D ∧ y ∈ ran ⁡ ball ⁡ D → ∃ b ∈ ran ⁡ ball ⁡ D z ∈ b ∧ b ⊆ x ∩ y ↔ ∃ r ∈ ℝ + z ball ⁡ D r ⊆ x ∩ y
12 1 11 mpbird ⊢ D ∈ ∞Met ⁡ X ∧ z ∈ x ∩ y ∧ x ∈ ran ⁡ ball ⁡ D ∧ y ∈ ran ⁡ ball ⁡ D → ∃ b ∈ ran ⁡ ball ⁡ D z ∈ b ∧ b ⊆ x ∩ y
13 12 ex ⊢ D ∈ ∞Met ⁡ X ∧ z ∈ x ∩ y → x ∈ ran ⁡ ball ⁡ D ∧ y ∈ ran ⁡ ball ⁡ D → ∃ b ∈ ran ⁡ ball ⁡ D z ∈ b ∧ b ⊆ x ∩ y
14 13 ralrimdva ⊢ D ∈ ∞Met ⁡ X → x ∈ ran ⁡ ball ⁡ D ∧ y ∈ ran ⁡ ball ⁡ D → ∀ z ∈ x ∩ y ∃ b ∈ ran ⁡ ball ⁡ D z ∈ b ∧ b ⊆ x ∩ y
15 14 ralrimivv ⊢ D ∈ ∞Met ⁡ X → ∀ x ∈ ran ⁡ ball ⁡ D ∀ y ∈ ran ⁡ ball ⁡ D ∀ z ∈ x ∩ y ∃ b ∈ ran ⁡ ball ⁡ D z ∈ 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 ⁡ D z ∈ 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 ⁡ D z ∈ b ∧ b ⊆ x ∩ y
20 15 19 sylibr ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ∈ TopBases