This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnmpt11

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 cnmptid.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt11.a 
|- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )
cnmpt11.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmpt11.b 
|- ( ph -> ( y e. Y |-> B ) e. ( K Cn L ) )
cnmpt11.c 
|- ( y = A -> B = C )
Assertion cnmpt11 
|- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )

Proof

Step Hyp Ref Expression
1 cnmptid.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmpt11.a 
 |-  ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )
3 cnmpt11.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
4 cnmpt11.b 
 |-  ( ph -> ( y e. Y |-> B ) e. ( K Cn L ) )
5 cnmpt11.c 
 |-  ( y = A -> B = C )
6 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
7 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ ( x e. X |-> A ) e. ( J Cn K ) ) -> ( x e. X |-> A ) : X --> Y )
8 1 3 2 7 syl3anc 
 |-  ( ph -> ( x e. X |-> A ) : X --> Y )
9 8 fvmptelcdm 
 |-  ( ( ph /\ x e. X ) -> A e. Y )
10 eqid 
 |-  ( x e. X |-> A ) = ( x e. X |-> A )
11 10 fvmpt2 
 |-  ( ( x e. X /\ A e. Y ) -> ( ( x e. X |-> A ) ` x ) = A )
12 6 9 11 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> A ) ` x ) = A )
13 12 fveq2d 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) = ( ( y e. Y |-> B ) ` A ) )
14 eqid 
 |-  ( y e. Y |-> B ) = ( y e. Y |-> B )
15 5 eleq1d 
 |-  ( y = A -> ( B e. U. L <-> C e. U. L ) )
16 cntop2 
 |-  ( ( y e. Y |-> B ) e. ( K Cn L ) -> L e. Top )
17 4 16 syl 
 |-  ( ph -> L e. Top )
18 toptopon2 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
19 17 18 sylib 
 |-  ( ph -> L e. ( TopOn ` U. L ) )
20 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` U. L ) /\ ( y e. Y |-> B ) e. ( K Cn L ) ) -> ( y e. Y |-> B ) : Y --> U. L )
21 3 19 4 20 syl3anc 
 |-  ( ph -> ( y e. Y |-> B ) : Y --> U. L )
22 14 fmpt 
 |-  ( A. y e. Y B e. U. L <-> ( y e. Y |-> B ) : Y --> U. L )
23 21 22 sylibr 
 |-  ( ph -> A. y e. Y B e. U. L )
24 23 adantr 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y B e. U. L )
25 15 24 9 rspcdva 
 |-  ( ( ph /\ x e. X ) -> C e. U. L )
26 14 5 9 25 fvmptd3 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y |-> B ) ` A ) = C )
27 13 26 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) = C )
28 fvco3 
 |-  ( ( ( x e. X |-> A ) : X --> Y /\ x e. X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) )
29 8 28 sylan 
 |-  ( ( ph /\ x e. X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) )
30 eqid 
 |-  ( x e. X |-> C ) = ( x e. X |-> C )
31 30 fvmpt2 
 |-  ( ( x e. X /\ C e. U. L ) -> ( ( x e. X |-> C ) ` x ) = C )
32 6 25 31 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> C ) ` x ) = C )
33 27 29 32 3eqtr4d 
 |-  ( ( ph /\ x e. X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) )
34 33 ralrimiva 
 |-  ( ph -> A. x e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) )
35 nfv 
 |-  F/ z ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x )
36 nfcv 
 |-  F/_ x ( y e. Y |-> B )
37 nfmpt1 
 |-  F/_ x ( x e. X |-> A )
38 36 37 nfco 
 |-  F/_ x ( ( y e. Y |-> B ) o. ( x e. X |-> A ) )
39 nfcv 
 |-  F/_ x z
40 38 39 nffv 
 |-  F/_ x ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z )
41 nfmpt1 
 |-  F/_ x ( x e. X |-> C )
42 41 39 nffv 
 |-  F/_ x ( ( x e. X |-> C ) ` z )
43 40 42 nfeq 
 |-  F/ x ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z )
44 fveq2 
 |-  ( x = z -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) )
45 fveq2 
 |-  ( x = z -> ( ( x e. X |-> C ) ` x ) = ( ( x e. X |-> C ) ` z ) )
46 44 45 eqeq12d 
 |-  ( x = z -> ( ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) <-> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) )
47 35 43 46 cbvralw 
 |-  ( A. x e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) <-> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) )
48 34 47 sylib 
 |-  ( ph -> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) )
49 fco 
 |-  ( ( ( y e. Y |-> B ) : Y --> U. L /\ ( x e. X |-> A ) : X --> Y ) -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) : X --> U. L )
50 21 8 49 syl2anc 
 |-  ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) : X --> U. L )
51 50 ffnd 
 |-  ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) Fn X )
52 25 fmpttd 
 |-  ( ph -> ( x e. X |-> C ) : X --> U. L )
53 52 ffnd 
 |-  ( ph -> ( x e. X |-> C ) Fn X )
54 eqfnfv 
 |-  ( ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) Fn X /\ ( x e. X |-> C ) Fn X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) <-> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) )
55 51 53 54 syl2anc 
 |-  ( ph -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) <-> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) )
56 48 55 mpbird 
 |-  ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) )
57 cnco 
 |-  ( ( ( x e. X |-> A ) e. ( J Cn K ) /\ ( y e. Y |-> B ) e. ( K Cn L ) ) -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) e. ( J Cn L ) )
58 2 4 57 syl2anc 
 |-  ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) e. ( J Cn L ) )
59 56 58 eqeltrrd 
 |-  ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )