Metamath Proof Explorer

Theorem cnpimaex

Description: Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006)

Ref Expression
Assertion cnpimaex 
|- ( ( F e. ( ( J CnP K ) ` P ) /\ A e. K /\ ( F ` P ) e. A ) -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 iscnp2 
 |-  ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. U. J ) /\ ( F : U. J --> U. K /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
4 3 simprbi 
 |-  ( F e. ( ( J CnP K ) ` P ) -> ( F : U. J --> U. K /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
5 eleq2 
 |-  ( y = A -> ( ( F ` P ) e. y <-> ( F ` P ) e. A ) )
6 sseq2 
 |-  ( y = A -> ( ( F " x ) C_ y <-> ( F " x ) C_ A ) )
7 6 anbi2d 
 |-  ( y = A -> ( ( P e. x /\ ( F " x ) C_ y ) <-> ( P e. x /\ ( F " x ) C_ A ) ) )
8 7 rexbidv 
 |-  ( y = A -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " x ) C_ A ) ) )
9 5 8 imbi12d 
 |-  ( y = A -> ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> ( ( F ` P ) e. A -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) ) ) )
10 9 rspccv 
 |-  ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( A e. K -> ( ( F ` P ) e. A -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) ) ) )
11 4 10 simpl2im 
 |-  ( F e. ( ( J CnP K ) ` P ) -> ( A e. K -> ( ( F ` P ) e. A -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) ) ) )
12 11 3imp 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ A e. K /\ ( F ` P ) e. A ) -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) )