Metamath Proof Explorer

Theorem cnmpt12f

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	$⊢ φ \to J \in TopOn (X)$
		cnmpt11.a	$⊢ φ \to (x \in X ⟼ A) \in (J Cn K)$
		cnmpt1t.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn L)$
		cnmpt12f.f	$⊢ φ \to F \in ((K \times_{t} L) Cn M)$
	Assertion	cnmpt12f	$⊢ φ \to (x \in X ⟼ A F B) \in (J Cn M)$

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt11.a	$⊢ φ \to (x \in X ⟼ A) \in (J Cn K)$
3		cnmpt1t.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn L)$
4		cnmpt12f.f	$⊢ φ \to F \in ((K \times_{t} L) Cn M)$
5		df-ov	$⊢ A F B = F (⟨A, B⟩)$
6	5	mpteq2i	$⊢ (x \in X ⟼ A F B) = (x \in X ⟼ F (⟨A, B⟩))$
7	1 2 3	cnmpt1t	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) \in (J Cn (K \times_{t} L))$
8	1 7 4	cnmpt11f	$⊢ φ \to (x \in X ⟼ F (⟨A, B⟩)) \in (J Cn M)$
9	6 8	eqeltrid	$⊢ φ \to (x \in X ⟼ A F B) \in (J Cn M)$