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 𝑓 ) ≠ ∅ } )