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