Metamath Proof Explorer

Theorem elmopn

Description: The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopnval.1 ⊢J=MetOpen⁡D
Assertion elmopn ⊢D∈∞Met⁡X→A∈J↔A⊆X∧∀x∈A∃y∈ran⁡ball⁡Dx∈y∧y⊆A

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢J=MetOpen⁡D
2 1 mopnval ⊢D∈∞Met⁡X→J=topGen⁡ran⁡ball⁡D
3 2 eleq2d ⊢D∈∞Met⁡X→A∈J↔A∈topGen⁡ran⁡ball⁡D
4 blbas ⊢D∈∞Met⁡X→ran⁡ball⁡D∈TopBases
5 eltg2 ⊢ran⁡ball⁡D∈TopBases→A∈topGen⁡ran⁡ball⁡D↔A⊆⋃ran⁡ball⁡D∧∀x∈A∃y∈ran⁡ball⁡Dx∈y∧y⊆A
6 4 5 syl ⊢D∈∞Met⁡X→A∈topGen⁡ran⁡ball⁡D↔A⊆⋃ran⁡ball⁡D∧∀x∈A∃y∈ran⁡ball⁡Dx∈y∧y⊆A
7 unirnbl ⊢D∈∞Met⁡X→⋃ran⁡ball⁡D=X
8 7 sseq2d ⊢D∈∞Met⁡X→A⊆⋃ran⁡ball⁡D↔A⊆X
9 8 anbi1d ⊢D∈∞Met⁡X→A⊆⋃ran⁡ball⁡D∧∀x∈A∃y∈ran⁡ball⁡Dx∈y∧y⊆A↔A⊆X∧∀x∈A∃y∈ran⁡ball⁡Dx∈y∧y⊆A
10 3 6 9 3bitrd ⊢D∈∞Met⁡X→A∈J↔A⊆X∧∀x∈A∃y∈ran⁡ball⁡Dx∈y∧y⊆A