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

Metamath Proof Explorer

Definition df-mopn

Description: Define a function whose value is the family of open sets of a metric space. See elmopn for its main property. (Contributed by NM, 1-Sep-2006)

Ref Expression
Assertion df-mopn MetOpen = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmopn ⊢ MetOpen
1 vd ⊢ 𝑑
2 cxmet ⊢ ∞Met
3 2 crn ⊢ ran ∞Met
4 3 cuni ⊢ ∪ ran ∞Met
5 ctg ⊢ topGen
6 cbl ⊢ ball
7 1 cv ⊢ 𝑑
8 7 6 cfv ⊢ ( ball ‘ 𝑑 )
9 8 crn ⊢ ran ( ball ‘ 𝑑 )
10 9 5 cfv ⊢ ( topGen ‘ ran ( ball ‘ 𝑑 ) )
11 1 4 10 cmpt ⊢ ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )
12 0 11 wceq ⊢ MetOpen = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )