Definition df-hcau

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau for its membership relation. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hcau	⊢ Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccauold	⊢ Cauchy
1		vf	⊢ 𝑓
2		chba	⊢ ℋ
3		cmap	⊢ ↑m
4		cn	⊢ ℕ
5	2 4 3	co	⊢ ( ℋ ↑m ℕ )
6		vx	⊢ 𝑥
7		crp	⊢ ℝ+
8		vy	⊢ 𝑦
9		vz	⊢ 𝑧
10		cuz	⊢ ℤ≥
11	8	cv	⊢ 𝑦
12	11 10	cfv	⊢ ( ℤ≥ ‘ 𝑦 )
13		cno	⊢ normℎ
14	1	cv	⊢ 𝑓
15	11 14	cfv	⊢ ( 𝑓 ‘ 𝑦 )
16		cmv	⊢ −ℎ
17	9	cv	⊢ 𝑧
18	17 14	cfv	⊢ ( 𝑓 ‘ 𝑧 )
19	15 18 16	co	⊢ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) )
20	19 13	cfv	⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) )
21		clt	⊢ <
22	6	cv	⊢ 𝑥
23	20 22 21	wbr	⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
24	23 9 12	wral	⊢ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
25	24 8 4	wrex	⊢ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
26	25 6 7	wral	⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥
27	26 1 5	crab	⊢ { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }
28	0 27	wceq	⊢ Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }