Metamath Proof Explorer

Theorem limcrcl

Description: Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion limcrcl 
|- ( C e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )

Proof

Step Hyp Ref Expression
1 df-limc 
 |-  limCC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` CCfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) } )
2 1 elmpocl 
 |-  ( C e. ( F limCC B ) -> ( F e. ( CC ^pm CC ) /\ B e. CC ) )
3 cnex 
 |-  CC e. _V
4 3 3 elpm2 
 |-  ( F e. ( CC ^pm CC ) <-> ( F : dom F --> CC /\ dom F C_ CC ) )
5 4 anbi1i 
 |-  ( ( F e. ( CC ^pm CC ) /\ B e. CC ) <-> ( ( F : dom F --> CC /\ dom F C_ CC ) /\ B e. CC ) )
6 df-3an 
 |-  ( ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) <-> ( ( F : dom F --> CC /\ dom F C_ CC ) /\ B e. CC ) )
7 5 6 bitr4i 
 |-  ( ( F e. ( CC ^pm CC ) /\ B e. CC ) <-> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
8 2 7 sylib 
 |-  ( C e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )