Metamath Proof Explorer

Theorem lmcl

Description: Closure of a limit. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 23-Dec-2013)

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

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 simp2d 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> P e. X )