Metamath Proof Explorer

Theorem lmfss

Description: Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 23-Dec-2013)

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

Proof

Step Hyp Ref Expression
1 lmfpm 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> F e. ( X ^pm CC ) )
2 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
3 cnex 
 |-  CC e. _V
4 elpmg 
 |-  ( ( X e. J /\ CC e. _V ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
5 2 3 4 sylancl 
 |-  ( J e. ( TopOn ` X ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
6 5 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
7 1 6 mpbid 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> ( Fun F /\ F C_ ( CC X. X ) ) )
8 7 simprd 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> F C_ ( CC X. X ) )