Metamath Proof Explorer

Theorem cnmpt22

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmpt21.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt21.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmpt21.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
cnmpt2t.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )
cnmpt22.l 
|- ( ph -> L e. ( TopOn ` Z ) )
cnmpt22.m 
|- ( ph -> M e. ( TopOn ` W ) )
cnmpt22.c 
|- ( ph -> ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) )
cnmpt22.d 
|- ( ( z = A /\ w = B ) -> C = D )
Assertion cnmpt22 
|- ( ph -> ( x e. X , y e. Y |-> D ) e. ( ( J tX K ) Cn N ) )

Proof

Step Hyp Ref Expression
1 cnmpt21.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmpt21.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmpt21.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
4 cnmpt2t.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )
5 cnmpt22.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
6 cnmpt22.m 
 |-  ( ph -> M e. ( TopOn ` W ) )
7 cnmpt22.c 
 |-  ( ph -> ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) )
8 cnmpt22.d 
 |-  ( ( z = A /\ w = B ) -> C = D )
9 df-ov 
 |-  ( A ( z e. Z , w e. W |-> C ) B ) = ( ( z e. Z , w e. W |-> C ) ` <. A , B >. )
10 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
11 1 2 10 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
12 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` Z ) /\ ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
13 11 5 3 12 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
14 eqid 
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
15 14 fmpo 
 |-  ( A. x e. X A. y e. Y A e. Z <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
16 13 15 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. Z )
17 rsp2 
 |-  ( A. x e. X A. y e. Y A e. Z -> ( ( x e. X /\ y e. Y ) -> A e. Z ) )
18 16 17 syl 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> A e. Z ) )
19 18 3impib 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> A e. Z )
20 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ M e. ( TopOn ` W ) /\ ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> W )
21 11 6 4 20 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> W )
22 eqid 
 |-  ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B )
23 22 fmpo 
 |-  ( A. x e. X A. y e. Y B e. W <-> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> W )
24 21 23 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y B e. W )
25 rsp2 
 |-  ( A. x e. X A. y e. Y B e. W -> ( ( x e. X /\ y e. Y ) -> B e. W ) )
26 24 25 syl 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> B e. W ) )
27 26 3impib 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> B e. W )
28 19 27 jca 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( A e. Z /\ B e. W ) )
29 txtopon 
 |-  ( ( L e. ( TopOn ` Z ) /\ M e. ( TopOn ` W ) ) -> ( L tX M ) e. ( TopOn ` ( Z X. W ) ) )
30 5 6 29 syl2anc 
 |-  ( ph -> ( L tX M ) e. ( TopOn ` ( Z X. W ) ) )
31 cntop2 
 |-  ( ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) -> N e. Top )
32 7 31 syl 
 |-  ( ph -> N e. Top )
33 toptopon2 
 |-  ( N e. Top <-> N e. ( TopOn ` U. N ) )
34 32 33 sylib 
 |-  ( ph -> N e. ( TopOn ` U. N ) )
35 cnf2 
 |-  ( ( ( L tX M ) e. ( TopOn ` ( Z X. W ) ) /\ N e. ( TopOn ` U. N ) /\ ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) ) -> ( z e. Z , w e. W |-> C ) : ( Z X. W ) --> U. N )
36 30 34 7 35 syl3anc 
 |-  ( ph -> ( z e. Z , w e. W |-> C ) : ( Z X. W ) --> U. N )
37 eqid 
 |-  ( z e. Z , w e. W |-> C ) = ( z e. Z , w e. W |-> C )
38 37 fmpo 
 |-  ( A. z e. Z A. w e. W C e. U. N <-> ( z e. Z , w e. W |-> C ) : ( Z X. W ) --> U. N )
39 36 38 sylibr 
 |-  ( ph -> A. z e. Z A. w e. W C e. U. N )
40 r2al 
 |-  ( A. z e. Z A. w e. W C e. U. N <-> A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) )
41 39 40 sylib 
 |-  ( ph -> A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) )
42 41 3ad2ant1 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) )
43 eleq1 
 |-  ( z = A -> ( z e. Z <-> A e. Z ) )
44 eleq1 
 |-  ( w = B -> ( w e. W <-> B e. W ) )
45 43 44 bi2anan9 
 |-  ( ( z = A /\ w = B ) -> ( ( z e. Z /\ w e. W ) <-> ( A e. Z /\ B e. W ) ) )
46 8 eleq1d 
 |-  ( ( z = A /\ w = B ) -> ( C e. U. N <-> D e. U. N ) )
47 45 46 imbi12d 
 |-  ( ( z = A /\ w = B ) -> ( ( ( z e. Z /\ w e. W ) -> C e. U. N ) <-> ( ( A e. Z /\ B e. W ) -> D e. U. N ) ) )
48 47 spc2gv 
 |-  ( ( A e. Z /\ B e. W ) -> ( A. z A. w ( ( z e. Z /\ w e. W ) -> C e. U. N ) -> ( ( A e. Z /\ B e. W ) -> D e. U. N ) ) )
49 28 42 28 48 syl3c 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> D e. U. N )
50 8 37 ovmpoga 
 |-  ( ( A e. Z /\ B e. W /\ D e. U. N ) -> ( A ( z e. Z , w e. W |-> C ) B ) = D )
51 19 27 49 50 syl3anc 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( z e. Z , w e. W |-> C ) B ) = D )
52 9 51 eqtr3id 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) = D )
53 52 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) ) = ( x e. X , y e. Y |-> D ) )
54 1 2 3 4 cnmpt2t 
 |-  ( ph -> ( x e. X , y e. Y |-> <. A , B >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
55 1 2 54 7 cnmpt21f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( ( z e. Z , w e. W |-> C ) ` <. A , B >. ) ) e. ( ( J tX K ) Cn N ) )
56 53 55 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> D ) e. ( ( J tX K ) Cn N ) )