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

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 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
hhlm.2 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
hhlm.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
hhcmpl.c ⊢ ( 𝐹 ∈ ( Cau ‘ 𝐷 ) → ∃ 𝑥 ∈ ℋ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
Assertion hhcmpl ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )

Proof

Step Hyp Ref Expression
1 hhlm.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhlm.2 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3 hhlm.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
4 hhcmpl.c ⊢ ( 𝐹 ∈ ( Cau ‘ 𝐷 ) → ∃ 𝑥 ∈ ℋ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 )
5 4 anim1ci ⊢ ( ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ ∃ 𝑥 ∈ ℋ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
6 elin ⊢ ( 𝐹 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) ) ↔ ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) )
7 r19.42v ⊢ ( ∃ 𝑥 ∈ ℋ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ ∃ 𝑥 ∈ ℋ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
8 5 6 7 3imtr4i ⊢ ( 𝐹 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) ) → ∃ 𝑥 ∈ ℋ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
9 1 2 hhcau ⊢ Cauchy = ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) )
10 9 eleq2i ⊢ ( 𝐹 ∈ Cauchy ↔ 𝐹 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) ) )
11 1 2 3 hhlm ⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑m ℕ ) )
12 11 breqi ⊢ ( 𝐹 ⇝𝑣 𝑥 ↔ 𝐹 ( ( ⇝𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 )
13 vex ⊢ 𝑥 ∈ V
14 13 brresi ⊢ ( 𝐹 ( ( ⇝𝑡 ‘ 𝐽 ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
15 12 14 bitri ⊢ ( 𝐹 ⇝𝑣 𝑥 ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
16 15 rexbii ⊢ ( ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 ↔ ∃ 𝑥 ∈ ℋ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
17 8 10 16 3imtr4i ⊢ ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )