Metamath Proof Explorer

Theorem iscnp2

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 Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses iscn.1 
|- X = U. J
iscn.2 
|- Y = U. K
Assertion iscnp2 
|- ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( 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 iscn.1 
 |-  X = U. J
2 iscn.2 
 |-  Y = U. K
3 n0i 
 |-  ( F e. ( ( J CnP K ) ` P ) -> -. ( ( J CnP K ) ` P ) = (/) )
4 df-ov 
 |-  ( J CnP K ) = ( CnP ` <. J , K >. )
5 ndmfv 
 |-  ( -. <. J , K >. e. dom CnP -> ( CnP ` <. J , K >. ) = (/) )
6 4 5 eqtrid 
 |-  ( -. <. J , K >. e. dom CnP -> ( J CnP K ) = (/) )
7 6 fveq1d 
 |-  ( -. <. J , K >. e. dom CnP -> ( ( J CnP K ) ` P ) = ( (/) ` P ) )
8 0fv 
 |-  ( (/) ` P ) = (/)
9 7 8 eqtrdi 
 |-  ( -. <. J , K >. e. dom CnP -> ( ( J CnP K ) ` P ) = (/) )
10 3 9 nsyl2 
 |-  ( F e. ( ( J CnP K ) ` P ) -> <. J , K >. e. dom CnP )
11 df-cnp 
 |-  CnP = ( j e. Top , k e. Top |-> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) )
12 ovex 
 |-  ( U. k ^m U. j ) e. _V
13 ssrab2 
 |-  { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } C_ ( U. k ^m U. j )
14 12 13 elpwi2 
 |-  { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } e. ~P ( U. k ^m U. j )
15 14 rgenw 
 |-  A. x e. U. j { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } e. ~P ( U. k ^m U. j )
16 eqid 
 |-  ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) = ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } )
17 16 fmpt 
 |-  ( A. x e. U. j { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } e. ~P ( U. k ^m U. j ) <-> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) : U. j --> ~P ( U. k ^m U. j ) )
18 15 17 mpbi 
 |-  ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) : U. j --> ~P ( U. k ^m U. j )
19 vuniex 
 |-  U. j e. _V
20 12 pwex 
 |-  ~P ( U. k ^m U. j ) e. _V
21 fex2 
 |-  ( ( ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) : U. j --> ~P ( U. k ^m U. j ) /\ U. j e. _V /\ ~P ( U. k ^m U. j ) e. _V ) -> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) e. _V )
22 18 19 20 21 mp3an 
 |-  ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) e. _V
23 11 22 dmmpo 
 |-  dom CnP = ( Top X. Top )
24 10 23 eleqtrdi 
 |-  ( F e. ( ( J CnP K ) ` P ) -> <. J , K >. e. ( Top X. Top ) )
25 opelxp 
 |-  ( <. J , K >. e. ( Top X. Top ) <-> ( J e. Top /\ K e. Top ) )
26 24 25 sylib 
 |-  ( F e. ( ( J CnP K ) ` P ) -> ( J e. Top /\ K e. Top ) )
27 26 simpld 
 |-  ( F e. ( ( J CnP K ) ` P ) -> J e. Top )
28 26 simprd 
 |-  ( F e. ( ( J CnP K ) ` P ) -> K e. Top )
29 elfvdm 
 |-  ( F e. ( ( J CnP K ) ` P ) -> P e. dom ( J CnP K ) )
30 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
31 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
32 cnpfval 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J CnP K ) = ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) )
33 30 31 32 syl2anb 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J CnP K ) = ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) )
34 26 33 syl 
 |-  ( F e. ( ( J CnP K ) ` P ) -> ( J CnP K ) = ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) )
35 34 dmeqd 
 |-  ( F e. ( ( J CnP K ) ` P ) -> dom ( J CnP K ) = dom ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) )
36 ovex 
 |-  ( Y ^m X ) e. _V
37 36 rabex 
 |-  { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } e. _V
38 37 rgenw 
 |-  A. x e. X { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } e. _V
39 dmmptg 
 |-  ( A. x e. X { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } e. _V -> dom ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) = X )
40 38 39 ax-mp 
 |-  dom ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) = X
41 35 40 eqtrdi 
 |-  ( F e. ( ( J CnP K ) ` P ) -> dom ( J CnP K ) = X )
42 29 41 eleqtrd 
 |-  ( F e. ( ( J CnP K ) ` P ) -> P e. X )
43 27 28 42 3jca 
 |-  ( F e. ( ( J CnP K ) ` P ) -> ( J e. Top /\ K e. Top /\ P e. X ) )
44 biid 
 |-  ( P e. X <-> P e. X )
45 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 ) ) ) ) )
46 30 31 44 45 syl3anb 
 |-  ( ( J e. Top /\ K e. Top /\ 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 ) ) ) ) )
47 43 46 biadanii 
 |-  ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )