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