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

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 ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ∈ TopBases )

Proof

Step Hyp Ref Expression
1 blin2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
2 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 elinel1 ⊢ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → 𝑧 ∈ 𝑥 )
4 elunii ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → 𝑧 ∈ ∪ ran ( ball ‘ 𝐷 ) )
5 3 4 sylan ⊢ ( ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → 𝑧 ∈ ∪ ran ( ball ‘ 𝐷 ) )
6 5 ad2ant2lr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑧 ∈ ∪ ran ( ball ‘ 𝐷 ) )
7 unirnbl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
8 7 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
9 6 8 eleqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑧 ∈ 𝑋 )
10 blssex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
11 2 9 10 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
12 1 11 mpbird ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
13 12 ex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
14 13 ralrimdva ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
15 14 ralrimivv ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
16 fvex ⊢ ( ball ‘ 𝐷 ) ∈ V
17 16 rnex ⊢ ran ( ball ‘ 𝐷 ) ∈ V
18 isbasis2g ⊢ ( ran ( ball ‘ 𝐷 ) ∈ V → ( ran ( ball ‘ 𝐷 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
19 17 18 ax-mp ⊢ ( ran ( ball ‘ 𝐷 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
20 15 19 sylibr ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ∈ TopBases )