This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )