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