Metamath Proof Explorer

Theorem iscnp

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscnp 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnpval 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( ( J CnP K ) ` P ) = { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } )
2 1 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> F e. { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } ) )
3 fveq1 
 |-  ( f = F -> ( f ` P ) = ( F ` P ) )
4 3 eleq1d 
 |-  ( f = F -> ( ( f ` P ) e. y <-> ( F ` P ) e. y ) )
5 imaeq1 
 |-  ( f = F -> ( f " x ) = ( F " x ) )
6 5 sseq1d 
 |-  ( f = F -> ( ( f " x ) C_ y <-> ( F " x ) C_ y ) )
7 6 anbi2d 
 |-  ( f = F -> ( ( P e. x /\ ( f " x ) C_ y ) <-> ( P e. x /\ ( F " x ) C_ y ) ) )
8 7 rexbidv 
 |-  ( f = F -> ( E. x e. J ( P e. x /\ ( f " x ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) )
9 4 8 imbi12d 
 |-  ( f = F -> ( ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) <-> ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
10 9 ralbidv 
 |-  ( f = F -> ( A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) <-> A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
11 10 elrab 
 |-  ( F e. { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } <-> ( F e. ( Y ^m X ) /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
12 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
13 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
14 elmapg 
 |-  ( ( Y e. K /\ X e. J ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
15 12 13 14 syl2anr 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
16 15 anbi1d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F e. ( Y ^m X ) /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
17 11 16 syl5bb 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
18 17 3adant3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
19 2 18 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )