Theorem hcau

Description: Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hcau	|- ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	|- ( f = F -> ( f ` y ) = ( F ` y ) )
2		fveq1	|- ( f = F -> ( f ` z ) = ( F ` z ) )
3	1 2	oveq12d	|- ( f = F -> ( ( f ` y ) -h ( f ` z ) ) = ( ( F ` y ) -h ( F ` z ) ) )
4	3	fveq2d	|- ( f = F -> ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) = ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) )
5	4	breq1d	|- ( f = F -> ( ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x <-> ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
6	5	rexralbidv	|- ( f = F -> ( E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x <-> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
7	6	ralbidv	|- ( f = F -> ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
8		df-hcau	|- Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }
9	7 8	elrab2	|- ( F e. Cauchy <-> ( F e. ( ~H ^m NN ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
10		ax-hilex	|- ~H e. _V
11		nnex	|- NN e. _V
12	10 11	elmap	|- ( F e. ( ~H ^m NN ) <-> F : NN --> ~H )
13	12	anbi1i	|- ( ( F e. ( ~H ^m NN ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
14	9 13	bitri	|- ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )