Metamath Proof Explorer

Theorem cnmpt21f

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	$⊢ φ \to J \in TopOn (X)$
		cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
		cnmpt21.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
		cnmpt21f.f	$⊢ φ \to F \in (L Cn M)$
	Assertion	cnmpt21f	$⊢ φ \to (x \in X, y \in Y ⟼ F (A)) \in ((J \times_{t} K) Cn M)$

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmpt21.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
4		cnmpt21f.f	$⊢ φ \to F \in (L Cn M)$
5		cntop1	$⊢ F \in (L Cn M) \to L \in Top$
6	4 5	syl	$⊢ φ \to L \in Top$
7		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
8	6 7	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
9		eqid	$⊢ ⋃ L = ⋃ L$
10		eqid	$⊢ ⋃ M = ⋃ M$
11	9 10	cnf	$⊢ F \in (L Cn M) \to F : ⋃ L ⟶ ⋃ M$
12	4 11	syl	$⊢ φ \to F : ⋃ L ⟶ ⋃ M$
13	12	feqmptd	$⊢ φ \to F = (z \in ⋃ L ⟼ F (z))$
14	13 4	eqeltrrd	$⊢ φ \to (z \in ⋃ L ⟼ F (z)) \in (L Cn M)$
15		fveq2	$⊢ z = A \to F (z) = F (A)$
16	1 2 3 8 14 15	cnmpt21	$⊢ φ \to (x \in X, y \in Y ⟼ F (A)) \in ((J \times_{t} K) Cn M)$