Metamath Proof Explorer

Theorem limcfval

Description: Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcval.j 
|- J = ( K |`t ( A u. { B } ) )
limcval.k 
|- K = ( TopOpen ` CCfld )
Assertion limcfval 
|- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( ( F limCC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } /\ ( F limCC B ) C_ CC ) )

Proof

Step Hyp Ref Expression
1 limcval.j 
 |-  J = ( K |`t ( A u. { B } ) )
2 limcval.k 
 |-  K = ( TopOpen ` CCfld )
3 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 ) } )
4 3 a1i 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> 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 ) } ) )
5 fvexd 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) -> ( TopOpen ` CCfld ) e. _V )
6 simplrl 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> f = F )
7 6 dmeqd 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> dom f = dom F )
8 simpll1 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> F : A --> CC )
9 8 fdmd 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> dom F = A )
10 7 9 eqtrd 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> dom f = A )
11 simplrr 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> x = B )
12 11 sneqd 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> { x } = { B } )
13 10 12 uneq12d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( dom f u. { x } ) = ( A u. { B } ) )
14 11 eqeq2d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( z = x <-> z = B ) )
15 6 fveq1d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( f ` z ) = ( F ` z ) )
16 14 15 ifbieq2d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> if ( z = x , y , ( f ` z ) ) = if ( z = B , y , ( F ` z ) ) )
17 13 16 mpteq12dv 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) )
18 simpr 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> j = ( TopOpen ` CCfld ) )
19 18 2 eqtr4di 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> j = K )
20 19 13 oveq12d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( j |`t ( dom f u. { x } ) ) = ( K |`t ( A u. { B } ) ) )
21 20 1 eqtr4di 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( j |`t ( dom f u. { x } ) ) = J )
22 21 19 oveq12d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( ( j |`t ( dom f u. { x } ) ) CnP j ) = ( J CnP K ) )
23 22 11 fveq12d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) = ( ( J CnP K ) ` B ) )
24 17 23 eleq12d 
 |-  ( ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) /\ j = ( TopOpen ` CCfld ) ) -> ( ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) ) )
25 5 24 sbcied 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) -> ( [. ( 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 ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) ) )
26 25 abbidv 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ ( f = F /\ x = B ) ) -> { 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 ) } = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } )
27 cnex 
 |-  CC e. _V
28 elpm2r 
 |-  ( ( ( CC e. _V /\ CC e. _V ) /\ ( F : A --> CC /\ A C_ CC ) ) -> F e. ( CC ^pm CC ) )
29 27 27 28 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ CC ) -> F e. ( CC ^pm CC ) )
30 29 3adant3 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> F e. ( CC ^pm CC ) )
31 simp3 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> B e. CC )
32 eqid 
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) )
33 1 2 32 limcvallem 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) -> y e. CC ) )
34 33 abssdv 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } C_ CC )
35 27 ssex 
 |-  ( { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } C_ CC -> { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } e. _V )
36 34 35 syl 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } e. _V )
37 4 26 30 31 36 ovmpod 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( F limCC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } )
38 37 34 eqsstrd 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( F limCC B ) C_ CC )
39 37 38 jca 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( ( F limCC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } /\ ( F limCC B ) C_ CC ) )