Metamath Proof Explorer

Theorem limcvallem

Description: Lemma for ellimc . (Contributed by Mario Carneiro, 25-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 limcval.j 
 |-  J = ( K |`t ( A u. { B } ) )
2 limcval.k 
 |-  K = ( TopOpen ` CCfld )
3 limcvallem.g 
 |-  G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )
4 iftrue 
 |-  ( z = B -> if ( z = B , C , ( F ` z ) ) = C )
5 4 eleq1d 
 |-  ( z = B -> ( if ( z = B , C , ( F ` z ) ) e. CC <-> C e. CC ) )
6 2 cnfldtopon 
 |-  K e. ( TopOn ` CC )
7 simpl2 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> A C_ CC )
8 simpl3 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> B e. CC )
9 8 snssd 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> { B } C_ CC )
10 7 9 unssd 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> ( A u. { B } ) C_ CC )
11 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ ( A u. { B } ) C_ CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
12 6 10 11 sylancr 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
13 1 12 eqeltrid 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> J e. ( TopOn ` ( A u. { B } ) ) )
14 6 a1i 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> K e. ( TopOn ` CC ) )
15 simpr 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> G e. ( ( J CnP K ) ` B ) )
16 cnpf2 
 |-  ( ( J e. ( TopOn ` ( A u. { B } ) ) /\ K e. ( TopOn ` CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> G : ( A u. { B } ) --> CC )
17 13 14 15 16 syl3anc 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> G : ( A u. { B } ) --> CC )
18 3 fmpt 
 |-  ( A. z e. ( A u. { B } ) if ( z = B , C , ( F ` z ) ) e. CC <-> G : ( A u. { B } ) --> CC )
19 17 18 sylibr 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> A. z e. ( A u. { B } ) if ( z = B , C , ( F ` z ) ) e. CC )
20 ssun2 
 |-  { B } C_ ( A u. { B } )
21 snssg 
 |-  ( B e. CC -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
22 8 21 syl 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
23 20 22 mpbiri 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> B e. ( A u. { B } ) )
24 5 19 23 rspcdva 
 |-  ( ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) /\ G e. ( ( J CnP K ) ` B ) ) -> C e. CC )
25 24 ex 
 |-  ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( G e. ( ( J CnP K ) ` B ) -> C e. CC ) )