This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) } )