Metamath Proof Explorer


Theorem cnpval

Description: The set of all functions from topology J to topology K that are continuous at a point P . (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Assertion 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 ) ) } )

Proof

Step Hyp Ref Expression
1 cnpfval
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J CnP K ) = ( v e. X |-> { f e. ( Y ^m X ) | A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v e. x /\ ( f " x ) C_ y ) ) } ) )
2 1 fveq1d
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( J CnP K ) ` P ) = ( ( v e. X |-> { f e. ( Y ^m X ) | A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v e. x /\ ( f " x ) C_ y ) ) } ) ` P ) )
3 fveq2
 |-  ( v = P -> ( f ` v ) = ( f ` P ) )
4 3 eleq1d
 |-  ( v = P -> ( ( f ` v ) e. y <-> ( f ` P ) e. y ) )
5 eleq1
 |-  ( v = P -> ( v e. x <-> P e. x ) )
6 5 anbi1d
 |-  ( v = P -> ( ( v e. x /\ ( f " x ) C_ y ) <-> ( P e. x /\ ( f " x ) C_ y ) ) )
7 6 rexbidv
 |-  ( v = P -> ( E. x e. J ( v e. x /\ ( f " x ) C_ y ) <-> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) )
8 4 7 imbi12d
 |-  ( v = P -> ( ( ( f ` v ) e. y -> E. x e. J ( v e. x /\ ( f " x ) C_ y ) ) <-> ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) ) )
9 8 ralbidv
 |-  ( v = P -> ( A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v 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 ) ) ) )
10 9 rabbidv
 |-  ( v = P -> { f e. ( Y ^m X ) | A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v 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 ) ) } )
11 eqid
 |-  ( v e. X |-> { f e. ( Y ^m X ) | A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v e. x /\ ( f " x ) C_ y ) ) } ) = ( v e. X |-> { f e. ( Y ^m X ) | A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v e. x /\ ( f " x ) C_ y ) ) } )
12 ovex
 |-  ( Y ^m X ) e. _V
13 12 rabex
 |-  { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } e. _V
14 10 11 13 fvmpt
 |-  ( P e. X -> ( ( v e. X |-> { f e. ( Y ^m X ) | A. y e. K ( ( f ` v ) e. y -> E. x e. J ( v e. x /\ ( f " x ) C_ y ) ) } ) ` 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 ) ) } )
15 2 14 sylan9eq
 |-  ( ( ( 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 ) ) } )
16 15 3impa
 |-  ( ( 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 ) ) } )