Theorem lmfpm

Description: If F converges, then F is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Assertion	lmfpm	|- ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> F e. ( X ^pm CC ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( J e. ( TopOn ` X ) -> J e. ( TopOn ` X ) )
2	1	lmbr	|- ( J e. ( TopOn ` X ) -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) ) )
3	2	biimpa	|- ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) )
4	3	simp1d	|- ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> F e. ( X ^pm CC ) )