Theorem hcau

Description: Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hcau	⊢ ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
2		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
3	1 2	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) )
4	3	fveq2d	⊢ ( 𝑓 = 𝐹 → ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) = ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
5	4	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 ↔ ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
6	5	rexralbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
7	6	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
8		df-hcau	⊢ Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 }
9	7 8	elrab2	⊢ ( 𝐹 ∈ Cauchy ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
10		ax-hilex	⊢ ℋ ∈ V
11		nnex	⊢ ℕ ∈ V
12	10 11	elmap	⊢ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ℋ )
13	12	anbi1i	⊢ ( ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
14	9 13	bitri	⊢ ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )