Metamath Proof Explorer

Theorem caufpm

Description: Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)

		Ref	Expression
	Assertion	caufpm	\|- ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> F e. ( X ^pm CC ) )

Proof

Step	Hyp	Ref	Expression
1		iscau	\|- ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. y e. ZZ ( F \|` ( ZZ>= ` y ) ) : ( ZZ>= ` y ) --> ( ( F ` y ) ( ball ` D ) x ) ) ) )
2	1	simprbda	\|- ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> F e. ( X ^pm CC ) )

Step

Hyp

Ref

Expression

iscau

 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. y e. ZZ ( F |` ( ZZ>= ` y ) ) : ( ZZ>= ` y ) --> ( ( F ` y ) ( ball ` D ) x ) ) ) )

simprbda

 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> F e. ( X ^pm CC ) )