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

Metamath Proof Explorer

Definition df-cmet

Description: Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014)

Ref Expression
Assertion df-cmet CMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmet ⊢ CMet
1 vx ⊢ 𝑥
2 cvv ⊢ V
3 vd ⊢ 𝑑
4 cmet ⊢ Met
5 1 cv ⊢ 𝑥
6 5 4 cfv ⊢ ( Met ‘ 𝑥 )
7 vf ⊢ 𝑓
8 ccfil ⊢ CauFil
9 3 cv ⊢ 𝑑
10 9 8 cfv ⊢ ( CauFil ‘ 𝑑 )
11 cmopn ⊢ MetOpen
12 9 11 cfv ⊢ ( MetOpen ‘ 𝑑 )
13 cflim ⊢ fLim
14 7 cv ⊢ 𝑓
15 12 14 13 co ⊢ ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 )
16 c0 ⊢ ∅
17 15 16 wne ⊢ ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅
18 17 7 10 wral ⊢ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅
19 18 3 6 crab ⊢ { 𝑑 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ }
20 1 2 19 cmpt ⊢ ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } )
21 0 20 wceq ⊢ CMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } )