cncfcompt2

Description: Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Step	Hyp	Ref	Expression
1		cncfcompt2.xph	$⊢ Ⅎ x φ$
2		cncfcompt2.ab	$⊢ φ \to (x \in A ⟼ R) : A \underset{cn}{⟶} B$
3		cncfcompt2.cd	$⊢ φ \to (y \in C ⟼ S) : C \underset{cn}{⟶} E$
4		cncfcompt2.bc	$⊢ φ \to B \subseteq C$
5		cncfcompt2.st	$⊢ y = R \to S = T$
6	4	adantr	$⊢ (φ \land x \in A) \to B \subseteq C$
7		cncff	$⊢ (x \in A ⟼ R) : A \underset{cn}{⟶} B \to (x \in A ⟼ R) : A ⟶ B$
8	2 7	syl	$⊢ φ \to (x \in A ⟼ R) : A ⟶ B$
9	8	fvmptelrn	$⊢ (φ \land x \in A) \to R \in B$
10	6 9	sseldd	$⊢ (φ \land x \in A) \to R \in C$
11	10	ex	$⊢ φ \to (x \in A \to R \in C)$
12	1 11	ralrimi	$⊢ φ \to \forall x \in A R \in C$
13		eqidd	$⊢ φ \to (x \in A ⟼ R) = (x \in A ⟼ R)$
14		eqidd	$⊢ φ \to (y \in C ⟼ S) = (y \in C ⟼ S)$
15	12 13 14 5	fmptcof	$⊢ φ \to (y \in C ⟼ S) \circ (x \in A ⟼ R) = (x \in A ⟼ T)$
16	15	eqcomd	$⊢ φ \to (x \in A ⟼ T) = (y \in C ⟼ S) \circ (x \in A ⟼ R)$
17		cncfrss	$⊢ (y \in C ⟼ S) : C \underset{cn}{⟶} E \to C \subseteq ℂ$
18	3 17	syl	$⊢ φ \to C \subseteq ℂ$
19		cncfss	$⊢ (B \subseteq C \land C \subseteq ℂ) \to A \underset{cn}{⟶} B \subseteq A \underset{cn}{⟶} C$
20	4 18 19	syl2anc	$⊢ φ \to A \underset{cn}{⟶} B \subseteq A \underset{cn}{⟶} C$
21	20 2	sseldd	$⊢ φ \to (x \in A ⟼ R) : A \underset{cn}{⟶} C$
22	21 3	cncfco	$⊢ φ \to ((y \in C ⟼ S) \circ (x \in A ⟼ R)) : A \underset{cn}{⟶} E$
23	16 22	eqeltrd	$⊢ φ \to (x \in A ⟼ T) : A \underset{cn}{⟶} E$

Metamath Proof Explorer