Axiom ax-hcompl

Description: Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hcompl	⊢ ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		ccauold	⊢ Cauchy
2	0 1	wcel	⊢ 𝐹 ∈ Cauchy
3		vx	⊢ 𝑥
4		chba	⊢ ℋ
5		chli	⊢ ⇝𝑣
6	3	cv	⊢ 𝑥
7	0 6 5	wbr	⊢ 𝐹 ⇝𝑣 𝑥
8	7 3 4	wrex	⊢ ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥
9	2 8	wi	⊢ ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )