Metamath Proof Explorer


Theorem cnmpt11f

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 φJTopOnX
cnmpt11.a φxXAJCnK
cnmpt11f.f φFKCnL
Assertion cnmpt11f φxXFAJCnL

Proof

Step Hyp Ref Expression
1 cnmptid.j φJTopOnX
2 cnmpt11.a φxXAJCnK
3 cnmpt11f.f φFKCnL
4 cntop2 xXAJCnKKTop
5 2 4 syl φKTop
6 toptopon2 KTopKTopOnK
7 5 6 sylib φKTopOnK
8 eqid K=K
9 eqid L=L
10 8 9 cnf FKCnLF:KL
11 3 10 syl φF:KL
12 11 feqmptd φF=yKFy
13 12 3 eqeltrrd φyKFyKCnL
14 fveq2 y=AFy=FA
15 1 2 7 13 14 cnmpt11 φxXFAJCnL