Metamath Proof Explorer


Theorem cnmptcom

Description: The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypotheses cnmptcom.3
|- ( ph -> J e. ( TopOn ` X ) )
cnmptcom.4
|- ( ph -> K e. ( TopOn ` Y ) )
cnmptcom.6
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
Assertion cnmptcom
|- ( ph -> ( y e. Y , x e. X |-> A ) e. ( ( K tX J ) Cn L ) )

Proof

Step Hyp Ref Expression
1 cnmptcom.3
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmptcom.4
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmptcom.6
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
4 txtopon
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
5 1 2 4 syl2anc
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
6 cntop2
 |-  ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) -> L e. Top )
7 3 6 syl
 |-  ( ph -> L e. Top )
8 toptopon2
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
9 7 8 sylib
 |-  ( ph -> L e. ( TopOn ` U. L ) )
10 cnf2
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` U. L ) /\ ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L )
11 5 9 3 10 syl3anc
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L )
12 eqid
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
13 12 fmpo
 |-  ( A. x e. X A. y e. Y A e. U. L <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L )
14 ralcom
 |-  ( A. x e. X A. y e. Y A e. U. L <-> A. y e. Y A. x e. X A e. U. L )
15 13 14 bitr3i
 |-  ( ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L <-> A. y e. Y A. x e. X A e. U. L )
16 11 15 sylib
 |-  ( ph -> A. y e. Y A. x e. X A e. U. L )
17 eqid
 |-  ( y e. Y , x e. X |-> A ) = ( y e. Y , x e. X |-> A )
18 17 fmpo
 |-  ( A. y e. Y A. x e. X A e. U. L <-> ( y e. Y , x e. X |-> A ) : ( Y X. X ) --> U. L )
19 16 18 sylib
 |-  ( ph -> ( y e. Y , x e. X |-> A ) : ( Y X. X ) --> U. L )
20 19 ffnd
 |-  ( ph -> ( y e. Y , x e. X |-> A ) Fn ( Y X. X ) )
21 fnov
 |-  ( ( y e. Y , x e. X |-> A ) Fn ( Y X. X ) <-> ( y e. Y , x e. X |-> A ) = ( z e. Y , w e. X |-> ( z ( y e. Y , x e. X |-> A ) w ) ) )
22 20 21 sylib
 |-  ( ph -> ( y e. Y , x e. X |-> A ) = ( z e. Y , w e. X |-> ( z ( y e. Y , x e. X |-> A ) w ) ) )
23 nfcv
 |-  F/_ y z
24 nfcv
 |-  F/_ x z
25 nfcv
 |-  F/_ x w
26 nfv
 |-  F/ y ph
27 nfcv
 |-  F/_ y x
28 nfmpo2
 |-  F/_ y ( x e. X , y e. Y |-> A )
29 27 28 23 nfov
 |-  F/_ y ( x ( x e. X , y e. Y |-> A ) z )
30 nfmpo1
 |-  F/_ y ( y e. Y , x e. X |-> A )
31 23 30 27 nfov
 |-  F/_ y ( z ( y e. Y , x e. X |-> A ) x )
32 29 31 nfeq
 |-  F/ y ( x ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) x )
33 26 32 nfim
 |-  F/ y ( ph -> ( x ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) x ) )
34 nfv
 |-  F/ x ph
35 nfmpo1
 |-  F/_ x ( x e. X , y e. Y |-> A )
36 25 35 24 nfov
 |-  F/_ x ( w ( x e. X , y e. Y |-> A ) z )
37 nfmpo2
 |-  F/_ x ( y e. Y , x e. X |-> A )
38 24 37 25 nfov
 |-  F/_ x ( z ( y e. Y , x e. X |-> A ) w )
39 36 38 nfeq
 |-  F/ x ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w )
40 34 39 nfim
 |-  F/ x ( ph -> ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w ) )
41 oveq2
 |-  ( y = z -> ( x ( x e. X , y e. Y |-> A ) y ) = ( x ( x e. X , y e. Y |-> A ) z ) )
42 oveq1
 |-  ( y = z -> ( y ( y e. Y , x e. X |-> A ) x ) = ( z ( y e. Y , x e. X |-> A ) x ) )
43 41 42 eqeq12d
 |-  ( y = z -> ( ( x ( x e. X , y e. Y |-> A ) y ) = ( y ( y e. Y , x e. X |-> A ) x ) <-> ( x ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) x ) ) )
44 43 imbi2d
 |-  ( y = z -> ( ( ph -> ( x ( x e. X , y e. Y |-> A ) y ) = ( y ( y e. Y , x e. X |-> A ) x ) ) <-> ( ph -> ( x ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) x ) ) ) )
45 oveq1
 |-  ( x = w -> ( x ( x e. X , y e. Y |-> A ) z ) = ( w ( x e. X , y e. Y |-> A ) z ) )
46 oveq2
 |-  ( x = w -> ( z ( y e. Y , x e. X |-> A ) x ) = ( z ( y e. Y , x e. X |-> A ) w ) )
47 45 46 eqeq12d
 |-  ( x = w -> ( ( x ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) x ) <-> ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w ) ) )
48 47 imbi2d
 |-  ( x = w -> ( ( ph -> ( x ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) x ) ) <-> ( ph -> ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w ) ) ) )
49 rsp2
 |-  ( A. y e. Y A. x e. X A e. U. L -> ( ( y e. Y /\ x e. X ) -> A e. U. L ) )
50 49 16 syl11
 |-  ( ( y e. Y /\ x e. X ) -> ( ph -> A e. U. L ) )
51 12 ovmpt4g
 |-  ( ( x e. X /\ y e. Y /\ A e. U. L ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
52 51 3com12
 |-  ( ( y e. Y /\ x e. X /\ A e. U. L ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
53 17 ovmpt4g
 |-  ( ( y e. Y /\ x e. X /\ A e. U. L ) -> ( y ( y e. Y , x e. X |-> A ) x ) = A )
54 52 53 eqtr4d
 |-  ( ( y e. Y /\ x e. X /\ A e. U. L ) -> ( x ( x e. X , y e. Y |-> A ) y ) = ( y ( y e. Y , x e. X |-> A ) x ) )
55 54 3expia
 |-  ( ( y e. Y /\ x e. X ) -> ( A e. U. L -> ( x ( x e. X , y e. Y |-> A ) y ) = ( y ( y e. Y , x e. X |-> A ) x ) ) )
56 50 55 syld
 |-  ( ( y e. Y /\ x e. X ) -> ( ph -> ( x ( x e. X , y e. Y |-> A ) y ) = ( y ( y e. Y , x e. X |-> A ) x ) ) )
57 23 24 25 33 40 44 48 56 vtocl2gaf
 |-  ( ( z e. Y /\ w e. X ) -> ( ph -> ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w ) ) )
58 57 com12
 |-  ( ph -> ( ( z e. Y /\ w e. X ) -> ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w ) ) )
59 58 3impib
 |-  ( ( ph /\ z e. Y /\ w e. X ) -> ( w ( x e. X , y e. Y |-> A ) z ) = ( z ( y e. Y , x e. X |-> A ) w ) )
60 59 mpoeq3dva
 |-  ( ph -> ( z e. Y , w e. X |-> ( w ( x e. X , y e. Y |-> A ) z ) ) = ( z e. Y , w e. X |-> ( z ( y e. Y , x e. X |-> A ) w ) ) )
61 22 60 eqtr4d
 |-  ( ph -> ( y e. Y , x e. X |-> A ) = ( z e. Y , w e. X |-> ( w ( x e. X , y e. Y |-> A ) z ) ) )
62 2 1 cnmpt2nd
 |-  ( ph -> ( z e. Y , w e. X |-> w ) e. ( ( K tX J ) Cn J ) )
63 2 1 cnmpt1st
 |-  ( ph -> ( z e. Y , w e. X |-> z ) e. ( ( K tX J ) Cn K ) )
64 2 1 62 63 3 cnmpt22f
 |-  ( ph -> ( z e. Y , w e. X |-> ( w ( x e. X , y e. Y |-> A ) z ) ) e. ( ( K tX J ) Cn L ) )
65 61 64 eqeltrd
 |-  ( ph -> ( y e. Y , x e. X |-> A ) e. ( ( K tX J ) Cn L ) )