Metamath Proof Explorer

Theorem cnfval

Description: The set of all continuous functions from topology J to topology K . (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnfval 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J Cn K ) = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )

Proof

Step Hyp Ref Expression
1 df-cn 
 |-  Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
2 1 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } ) )
3 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> k = K )
4 3 unieqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. k = U. K )
5 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
6 5 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> Y = U. K )
7 4 6 eqtr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. k = Y )
8 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> j = J )
9 8 unieqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. j = U. J )
10 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
11 10 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> X = U. J )
12 9 11 eqtr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> U. j = X )
13 7 12 oveq12d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( U. k ^m U. j ) = ( Y ^m X ) )
14 8 eleq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( ( `' f " y ) e. j <-> ( `' f " y ) e. J ) )
15 3 14 raleqbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> ( A. y e. k ( `' f " y ) e. j <-> A. y e. K ( `' f " y ) e. J ) )
16 13 15 rabeqbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( j = J /\ k = K ) ) -> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )
17 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
18 17 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> J e. Top )
19 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
20 19 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> K e. Top )
21 ovex 
 |-  ( Y ^m X ) e. _V
22 21 rabex 
 |-  { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } e. _V
23 22 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } e. _V )
24 2 16 18 20 23 ovmpod 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J Cn K ) = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )