Theorem lmrcl

Description: Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015)

	Ref	Expression
Assertion	lmrcl	|- ( F ( ~~>t ` J ) P -> J e. Top )

Proof

Step	Hyp	Ref	Expression
1		df-lm	|- ~~>t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
2	1	dmmptss	|- dom ~~>t C_ Top
3		df-br	|- ( F ( ~~>t ` J ) P <-> <. F , P >. e. ( ~~>t ` J ) )
4		elfvdm	|- ( <. F , P >. e. ( ~~>t ` J ) -> J e. dom ~~>t )
5	3 4	sylbi	|- ( F ( ~~>t ` J ) P -> J e. dom ~~>t )
6	2 5	sselid	|- ( F ( ~~>t ` J ) P -> J e. Top )