Metamath Proof Explorer


Theorem cnmpt21

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 φ J TopOn X
cnmpt21.k φ K TopOn Y
cnmpt21.a φ x X , y Y A J × t K Cn L
cnmpt21.l φ L TopOn Z
cnmpt21.b φ z Z B L Cn M
cnmpt21.c z = A B = C
Assertion cnmpt21 φ x X , y Y C J × t K Cn M

Proof

Step Hyp Ref Expression
1 cnmpt21.j φ J TopOn X
2 cnmpt21.k φ K TopOn Y
3 cnmpt21.a φ x X , y Y A J × t K Cn L
4 cnmpt21.l φ L TopOn Z
5 cnmpt21.b φ z Z B L Cn M
6 cnmpt21.c z = A B = C
7 df-ov x x X , y Y A y = x X , y Y A x y
8 simprl φ x X y Y x X
9 simprr φ x X y Y y Y
10 txtopon J TopOn X K TopOn Y J × t K TopOn X × Y
11 1 2 10 syl2anc φ J × t K TopOn X × Y
12 cnf2 J × t K TopOn X × Y L TopOn Z x X , y Y A J × t K Cn L x X , y Y A : X × Y Z
13 11 4 3 12 syl3anc φ x X , y Y A : X × Y Z
14 eqid x X , y Y A = x X , y Y A
15 14 fmpo x X y Y A Z x X , y Y A : X × Y Z
16 13 15 sylibr φ x X y Y A Z
17 rsp2 x X y Y A Z x X y Y A Z
18 16 17 syl φ x X y Y A Z
19 18 imp φ x X y Y A Z
20 14 ovmpt4g x X y Y A Z x x X , y Y A y = A
21 8 9 19 20 syl3anc φ x X y Y x x X , y Y A y = A
22 7 21 eqtr3id φ x X y Y x X , y Y A x y = A
23 22 fveq2d φ x X y Y z Z B x X , y Y A x y = z Z B A
24 eqid z Z B = z Z B
25 6 eleq1d z = A B M C M
26 cntop2 z Z B L Cn M M Top
27 5 26 syl φ M Top
28 toptopon2 M Top M TopOn M
29 27 28 sylib φ M TopOn M
30 cnf2 L TopOn Z M TopOn M z Z B L Cn M z Z B : Z M
31 4 29 5 30 syl3anc φ z Z B : Z M
32 24 fmpt z Z B M z Z B : Z M
33 31 32 sylibr φ z Z B M
34 33 adantr φ x X y Y z Z B M
35 25 34 19 rspcdva φ x X y Y C M
36 24 6 19 35 fvmptd3 φ x X y Y z Z B A = C
37 23 36 eqtrd φ x X y Y z Z B x X , y Y A x y = C
38 opelxpi x X y Y x y X × Y
39 fvco3 x X , y Y A : X × Y Z x y X × Y z Z B x X , y Y A x y = z Z B x X , y Y A x y
40 13 38 39 syl2an φ x X y Y z Z B x X , y Y A x y = z Z B x X , y Y A x y
41 df-ov x x X , y Y C y = x X , y Y C x y
42 eqid x X , y Y C = x X , y Y C
43 42 ovmpt4g x X y Y C M x x X , y Y C y = C
44 8 9 35 43 syl3anc φ x X y Y x x X , y Y C y = C
45 41 44 eqtr3id φ x X y Y x X , y Y C x y = C
46 37 40 45 3eqtr4d φ x X y Y z Z B x X , y Y A x y = x X , y Y C x y
47 46 ralrimivva φ x X y Y z Z B x X , y Y A x y = x X , y Y C x y
48 nfv u y Y z Z B x X , y Y A x y = x X , y Y C x y
49 nfcv _ x Y
50 nfcv _ x z Z B
51 nfmpo1 _ x x X , y Y A
52 50 51 nfco _ x z Z B x X , y Y A
53 nfcv _ x u v
54 52 53 nffv _ x z Z B x X , y Y A u v
55 nfmpo1 _ x x X , y Y C
56 55 53 nffv _ x x X , y Y C u v
57 54 56 nfeq x z Z B x X , y Y A u v = x X , y Y C u v
58 49 57 nfralw x v Y z Z B x X , y Y A u v = x X , y Y C u v
59 nfv v z Z B x X , y Y A x y = x X , y Y C x y
60 nfcv _ y z Z B
61 nfmpo2 _ y x X , y Y A
62 60 61 nfco _ y z Z B x X , y Y A
63 nfcv _ y x v
64 62 63 nffv _ y z Z B x X , y Y A x v
65 nfmpo2 _ y x X , y Y C
66 65 63 nffv _ y x X , y Y C x v
67 64 66 nfeq y z Z B x X , y Y A x v = x X , y Y C x v
68 opeq2 y = v x y = x v
69 68 fveq2d y = v z Z B x X , y Y A x y = z Z B x X , y Y A x v
70 68 fveq2d y = v x X , y Y C x y = x X , y Y C x v
71 69 70 eqeq12d y = v z Z B x X , y Y A x y = x X , y Y C x y z Z B x X , y Y A x v = x X , y Y C x v
72 59 67 71 cbvralw y Y z Z B x X , y Y A x y = x X , y Y C x y v Y z Z B x X , y Y A x v = x X , y Y C x v
73 opeq1 x = u x v = u v
74 73 fveq2d x = u z Z B x X , y Y A x v = z Z B x X , y Y A u v
75 73 fveq2d x = u x X , y Y C x v = x X , y Y C u v
76 74 75 eqeq12d x = u z Z B x X , y Y A x v = x X , y Y C x v z Z B x X , y Y A u v = x X , y Y C u v
77 76 ralbidv x = u v Y z Z B x X , y Y A x v = x X , y Y C x v v Y z Z B x X , y Y A u v = x X , y Y C u v
78 72 77 syl5bb x = u y Y z Z B x X , y Y A x y = x X , y Y C x y v Y z Z B x X , y Y A u v = x X , y Y C u v
79 48 58 78 cbvralw x X y Y z Z B x X , y Y A x y = x X , y Y C x y u X v Y z Z B x X , y Y A u v = x X , y Y C u v
80 47 79 sylib φ u X v Y z Z B x X , y Y A u v = x X , y Y C u v
81 fveq2 w = u v z Z B x X , y Y A w = z Z B x X , y Y A u v
82 fveq2 w = u v x X , y Y C w = x X , y Y C u v
83 81 82 eqeq12d w = u v z Z B x X , y Y A w = x X , y Y C w z Z B x X , y Y A u v = x X , y Y C u v
84 83 ralxp w X × Y z Z B x X , y Y A w = x X , y Y C w u X v Y z Z B x X , y Y A u v = x X , y Y C u v
85 80 84 sylibr φ w X × Y z Z B x X , y Y A w = x X , y Y C w
86 fco z Z B : Z M x X , y Y A : X × Y Z z Z B x X , y Y A : X × Y M
87 31 13 86 syl2anc φ z Z B x X , y Y A : X × Y M
88 87 ffnd φ z Z B x X , y Y A Fn X × Y
89 35 ralrimivva φ x X y Y C M
90 42 fmpo x X y Y C M x X , y Y C : X × Y M
91 89 90 sylib φ x X , y Y C : X × Y M
92 91 ffnd φ x X , y Y C Fn X × Y
93 eqfnfv z Z B x X , y Y A Fn X × Y x X , y Y C Fn X × Y z Z B x X , y Y A = x X , y Y C w X × Y z Z B x X , y Y A w = x X , y Y C w
94 88 92 93 syl2anc φ z Z B x X , y Y A = x X , y Y C w X × Y z Z B x X , y Y A w = x X , y Y C w
95 85 94 mpbird φ z Z B x X , y Y A = x X , y Y C
96 cnco x X , y Y A J × t K Cn L z Z B L Cn M z Z B x X , y Y A J × t K Cn M
97 3 5 96 syl2anc φ z Z B x X , y Y A J × t K Cn M
98 95 97 eqeltrrd φ x X , y Y C J × t K Cn M