Metamath Proof Explorer

Theorem cnpfval

Description: The function mapping the points in a topology J to the set of all functions from J to topology K continuous at that point. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 df-cnp 
 |-  CnP = ( j e. Top , k e. Top |-> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. w e. k ( ( f ` x ) e. w -> E. v e. j ( x e. v /\ ( f " v ) C_ w ) ) } ) )
2 1 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> CnP = ( j e. Top , k e. Top |-> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. w e. k ( ( f ` x ) e. w -> E. v e. j ( x e. v /\ ( f " v ) C_ w ) ) } ) ) )
3 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> j = J )
4 3 unieqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. j = U. J )
5 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
6 5 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> X = U. J )
7 4 6 eqtr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. j = X )
8 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> k = K )
9 8 unieqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. k = U. K )
10 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
11 10 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> Y = U. K )
12 9 11 eqtr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. k = Y )
13 12 7 oveq12d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( U. k ^m U. j ) = ( Y ^m X ) )
14 3 rexeqdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( E. v e. j ( x e. v /\ ( f " v ) C_ w ) <-> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) )
15 14 imbi2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( ( ( f ` x ) e. w -> E. v e. j ( x e. v /\ ( f " v ) C_ w ) ) <-> ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) ) )
16 8 15 raleqbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( A. w e. k ( ( f ` x ) e. w -> E. v e. j ( x e. v /\ ( f " v ) C_ w ) ) <-> A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) ) )
17 13 16 rabeqbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> { f e. ( U. k ^m U. j ) | A. w e. k ( ( f ` x ) e. w -> E. v e. j ( x e. v /\ ( f " v ) C_ w ) ) } = { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } )
18 7 17 mpteq12dv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. w e. k ( ( f ` x ) e. w -> E. v e. j ( x e. v /\ ( f " v ) C_ w ) ) } ) = ( 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 ) ) } ) )
19 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
20 19 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> J e. Top )
21 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
22 21 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> K e. Top )
23 ovex 
 |-  ( Y ^m X ) e. _V
24 ssrab2 
 |-  { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } C_ ( Y ^m X )
25 23 24 elpwi2 
 |-  { 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. ~P ( Y ^m X )
26 25 a1i 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ 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. ~P ( Y ^m X ) )
27 26 fmpttd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( 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 --> ~P ( Y ^m X ) )
28 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
29 28 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> X e. J )
30 23 pwex 
 |-  ~P ( Y ^m X ) e. _V
31 30 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ~P ( Y ^m X ) e. _V )
32 fex2 
 |-  ( ( ( 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 --> ~P ( Y ^m X ) /\ X e. J /\ ~P ( Y ^m X ) e. _V ) -> ( 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 )
33 27 29 31 32 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( 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 )
34 2 18 20 22 33 ovmpod 
 |-  ( ( 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 ) ) } ) )