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	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	cnmpt11.a	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(J\mathrm{Cn}K\right)$$
	cnmpt11f.f	$$⊢\phi \to F\in \left(K\mathrm{Cn}L\right)$$
Assertion	cnmpt11f	$$⊢\phi \to \left(x\in X⟼F\left(A\right)\right)\in \left(J\mathrm{Cn}L\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
2		cnmpt11.a	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(J\mathrm{Cn}K\right)$$
3		cnmpt11f.f	$$⊢\phi \to F\in \left(K\mathrm{Cn}L\right)$$
4		cntop2	$$⊢\left(x\in X⟼A\right)\in \left(J\mathrm{Cn}K\right)\to K\in \mathrm{Top}$$
5	2 4	syl	$$⊢\phi \to K\in \mathrm{Top}$$
6		toptopon2	$$⊢K\in \mathrm{Top}\leftrightarrow K\in \mathrm{TopOn}\left(\bigcup K\right)$$
7	5 6	sylib	$$⊢\phi \to K\in \mathrm{TopOn}\left(\bigcup K\right)$$
8		eqid	$$⊢\bigcup K=\bigcup K$$
9		eqid	$$⊢\bigcup L=\bigcup L$$
10	8 9	cnf	$$⊢F\in \left(K\mathrm{Cn}L\right)\to F:\bigcup K⟶\bigcup L$$
11	3 10	syl	$$⊢\phi \to F:\bigcup K⟶\bigcup L$$
12	11	feqmptd	$$⊢\phi \to F=\left(y\in \bigcup K⟼F\left(y\right)\right)$$
13	12 3	eqeltrrd	$$⊢\phi \to \left(y\in \bigcup K⟼F\left(y\right)\right)\in \left(K\mathrm{Cn}L\right)$$
14		fveq2	$$⊢y=A\to F\left(y\right)=F\left(A\right)$$
15	1 2 7 13 14	cnmpt11	$$⊢\phi \to \left(x\in X⟼F\left(A\right)\right)\in \left(J\mathrm{Cn}L\right)$$