Axiom ax-hcompl

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

	Ref	Expression
Assertion	ax-hcompl	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		ccauold	$$class\mathrm{Cauchy}$$
2	0 1	wcel	$$wffF\in \mathrm{Cauchy}$$
3		vx	$$setvarx$$
4		chba	$$class\mathscr{H}$$
5		chli	$$class\underset{v}{⇝}$$
6	3	cv	$$setvarx$$
7	0 6 5	wbr	$$wffF\underset{v}{⇝}x$$
8	7 3 4	wrex	$$wff\exists x\in \mathscr{H}F\underset{v}{⇝}x$$
9	2 8	wi	$$wff\left(F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x\right)$$