Metamath Proof Explorer

Theorem limccl

Description: Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Assertion limccl 
|- ( F limCC B ) C_ CC

Proof

Step Hyp Ref Expression
1 limcrcl 
 |-  ( x e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
2 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( dom F u. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( dom F u. { B } ) )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 2 3 limcfval 
 |-  ( ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) -> ( ( F limCC B ) = { y | ( z e. ( dom F u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( dom F u. { B } ) ) CnP ( TopOpen ` CCfld ) ) ` B ) } /\ ( F limCC B ) C_ CC ) )
5 1 4 syl 
 |-  ( x e. ( F limCC B ) -> ( ( F limCC B ) = { y | ( z e. ( dom F u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( dom F u. { B } ) ) CnP ( TopOpen ` CCfld ) ) ` B ) } /\ ( F limCC B ) C_ CC ) )
6 5 simprd 
 |-  ( x e. ( F limCC B ) -> ( F limCC B ) C_ CC )
7 id 
 |-  ( x e. ( F limCC B ) -> x e. ( F limCC B ) )
8 6 7 sseldd 
 |-  ( x e. ( F limCC B ) -> x e. CC )
9 8 ssriv 
 |-  ( F limCC B ) C_ CC