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 = <. <. +h , .h >. , normh >.
	hhlm.2	|- D = ( IndMet ` U )
	hhlm.3	|- J = ( MetOpen ` D )
	hhcmpl.c	|- ( F e. ( Cau ` D ) -> E. x e. ~H F ( ~~>t ` J ) x )
Assertion	hhcmpl	|- ( F e. Cauchy -> E. x e. ~H F ~~>v x )

Proof

Step	Hyp	Ref	Expression
1		hhlm.1	|- U = <. <. +h , .h >. , normh >.
2		hhlm.2	|- D = ( IndMet ` U )
3		hhlm.3	|- J = ( MetOpen ` D )
4		hhcmpl.c	|- ( F e. ( Cau ` D ) -> E. x e. ~H F ( ~~>t ` J ) x )
5	4	anim1ci	|- ( ( F e. ( Cau ` D ) /\ F e. ( ~H ^m NN ) ) -> ( F e. ( ~H ^m NN ) /\ E. x e. ~H F ( ~~>t ` J ) x ) )
6		elin	|- ( F e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( F e. ( Cau ` D ) /\ F e. ( ~H ^m NN ) ) )
7		r19.42v	|- ( E. x e. ~H ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` J ) x ) <-> ( F e. ( ~H ^m NN ) /\ E. x e. ~H F ( ~~>t ` J ) x ) )
8	5 6 7	3imtr4i	|- ( F e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) -> E. x e. ~H ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` J ) x ) )
9	1 2	hhcau	|- Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) )
10	9	eleq2i	|- ( F e. Cauchy <-> F e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) )
11	1 2 3	hhlm	|- ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )
12	11	breqi	|- ( F ~~>v x <-> F ( ( ~~>t ` J ) |` ( ~H ^m NN ) ) x )
13		vex	|- x e. _V
14	13	brresi	|- ( F ( ( ~~>t ` J ) |` ( ~H ^m NN ) ) x <-> ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` J ) x ) )
15	12 14	bitri	|- ( F ~~>v x <-> ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` J ) x ) )
16	15	rexbii	|- ( E. x e. ~H F ~~>v x <-> E. x e. ~H ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` J ) x ) )
17	8 10 16	3imtr4i	|- ( F e. Cauchy -> E. x e. ~H F ~~>v x )