Definition df-cau

Description: Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006)

	Ref	Expression
Assertion	df-cau	⊢ Cau = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccau	⊢ Cau
1		vd	⊢ 𝑑
2		cxmet	⊢ ∞Met
3	2	crn	⊢ ran ∞Met
4	3	cuni	⊢ ∪ ran ∞Met
5		vf	⊢ 𝑓
6	1	cv	⊢ 𝑑
7	6	cdm	⊢ dom 𝑑
8	7	cdm	⊢ dom dom 𝑑
9		cpm	⊢ ↑pm
10		cc	⊢ ℂ
11	8 10 9	co	⊢ ( dom dom 𝑑 ↑pm ℂ )
12		vx	⊢ 𝑥
13		crp	⊢ ℝ+
14		vj	⊢ 𝑗
15		cz	⊢ ℤ
16	5	cv	⊢ 𝑓
17		cuz	⊢ ℤ≥
18	14	cv	⊢ 𝑗
19	18 17	cfv	⊢ ( ℤ≥ ‘ 𝑗 )
20	16 19	cres	⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) )
21	18 16	cfv	⊢ ( 𝑓 ‘ 𝑗 )
22		cbl	⊢ ball
23	6 22	cfv	⊢ ( ball ‘ 𝑑 )
24	12	cv	⊢ 𝑥
25	21 24 23	co	⊢ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
26	19 25 20	wf	⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
27	26 14 15	wrex	⊢ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
28	27 12 13	wral	⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
29	28 5 11	crab	⊢ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) }
30	1 4 29	cmpt	⊢ ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) } )
31	0 30	wceq	⊢ Cau = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) } )