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

Metamath Proof Explorer

Theorem hlcompl

Description: Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007) (Revised by Mario Carneiro, 9-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hlcompl.1 ⊢ D = IndMet ⁡ U
hlcompl.2 ⊢ J = MetOpen ⁡ D
Assertion hlcompl ⊢ U ∈ CHil OLD ∧ F ∈ Cau ⁡ D → F ∈ dom ⁡ ⇝t ⁡ J

Proof

Step Hyp Ref Expression
1 hlcompl.1 ⊢ D = IndMet ⁡ U
2 hlcompl.2 ⊢ J = MetOpen ⁡ D
3 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
4 3 1 hlcmet ⊢ U ∈ CHil OLD → D ∈ CMet ⁡ BaseSet ⁡ U
5 2 cmetcau ⊢ D ∈ CMet ⁡ BaseSet ⁡ U ∧ F ∈ Cau ⁡ D → F ∈ dom ⁡ ⇝t ⁡ J
6 4 5 sylan ⊢ U ∈ CHil OLD ∧ F ∈ Cau ⁡ D → F ∈ dom ⁡ ⇝t ⁡ J