Metamath Proof Explorer

Theorem hhcmpl

Description: Lemma used for derivation of the completeness axiom ax-hcompl from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhlm.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
hhlm.2 ⊢ D = IndMet ⁡ U
hhlm.3 ⊢ J = MetOpen ⁡ D
hhcmpl.c ⊢ F ∈ Cau ⁡ D → ∃ x ∈ ℋ F ⇝t ⁡ J x
Assertion hhcmpl ⊢ F ∈ Cauchy → ∃ x ∈ ℋ F ⇝v x

Proof

Step Hyp Ref Expression
1 hhlm.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hhlm.2 ⊢ D = IndMet ⁡ U
3 hhlm.3 ⊢ J = MetOpen ⁡ D
4 hhcmpl.c ⊢ F ∈ Cau ⁡ D → ∃ x ∈ ℋ F ⇝t ⁡ J x
5 4 anim1ci ⊢ F ∈ Cau ⁡ D ∧ F ∈ ℋ ℕ → F ∈ ℋ ℕ ∧ ∃ x ∈ ℋ F ⇝t ⁡ J x
6 elin ⊢ F ∈ Cau ⁡ D ∩ ℋ ℕ ↔ F ∈ Cau ⁡ D ∧ F ∈ ℋ ℕ
7 r19.42v ⊢ ∃ x ∈ ℋ F ∈ ℋ ℕ ∧ F ⇝t ⁡ J x ↔ F ∈ ℋ ℕ ∧ ∃ x ∈ ℋ F ⇝t ⁡ J x
8 5 6 7 3imtr4i ⊢ F ∈ Cau ⁡ D ∩ ℋ ℕ → ∃ x ∈ ℋ F ∈ ℋ ℕ ∧ F ⇝t ⁡ J x
9 1 2 hhcau ⊢ Cauchy = Cau ⁡ D ∩ ℋ ℕ
10 9 eleq2i ⊢ F ∈ Cauchy ↔ F ∈ Cau ⁡ D ∩ ℋ ℕ
11 1 2 3 hhlm ⊢ ⇝v = ⇝t ⁡ J ↾ ℋ ℕ
12 11 breqi ⊢ F ⇝v x ↔ F ⇝t ⁡ J ↾ ℋ ℕ x
13 vex ⊢ x ∈ V
14 13 brresi ⊢ F ⇝t ⁡ J ↾ ℋ ℕ x ↔ F ∈ ℋ ℕ ∧ F ⇝t ⁡ J x
15 12 14 bitri ⊢ F ⇝v x ↔ F ∈ ℋ ℕ ∧ F ⇝t ⁡ J x
16 15 rexbii ⊢ ∃ x ∈ ℋ F ⇝v x ↔ ∃ x ∈ ℋ F ∈ ℋ ℕ ∧ F ⇝t ⁡ J x
17 8 10 16 3imtr4i ⊢ F ∈ Cauchy → ∃ x ∈ ℋ F ⇝v x