Metamath Proof Explorer

Theorem mopni

Description: An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopni.1 ⊢J=MetOpen⁡D
Assertion mopni ⊢D∈∞Met⁡X∧A∈J∧P∈A→∃x∈ran⁡ball⁡DP∈x∧x⊆A

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢J=MetOpen⁡D
2 1 elmopn ⊢D∈∞Met⁡X→A∈J↔A⊆X∧∀y∈A∃x∈ran⁡ball⁡Dy∈x∧x⊆A
3 2 simplbda ⊢D∈∞Met⁡X∧A∈J→∀y∈A∃x∈ran⁡ball⁡Dy∈x∧x⊆A
4 eleq1 ⊢y=P→y∈x↔P∈x
5 4 anbi1d ⊢y=P→y∈x∧x⊆A↔P∈x∧x⊆A
6 5 rexbidv ⊢y=P→∃x∈ran⁡ball⁡Dy∈x∧x⊆A↔∃x∈ran⁡ball⁡DP∈x∧x⊆A
7 6 rspccv ⊢∀y∈A∃x∈ran⁡ball⁡Dy∈x∧x⊆A→P∈A→∃x∈ran⁡ball⁡DP∈x∧x⊆A
8 3 7 syl ⊢D∈∞Met⁡X∧A∈J→P∈A→∃x∈ran⁡ball⁡DP∈x∧x⊆A
9 8 3impia ⊢D∈∞Met⁡X∧A∈J∧P∈A→∃x∈ran⁡ball⁡DP∈x∧x⊆A