cncfcompt

Description: Composition of continuous functions. A generalization of cncfmpt1f to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfcompt.bcn	$⊢ φ \to (x \in A ⟼ B) : A \underset{cn}{⟶} C$
	cncfcompt.f	$⊢ φ \to F : C \underset{cn}{⟶} D$
Assertion	cncfcompt	$⊢ φ \to (x \in A ⟼ F (B)) : A \underset{cn}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		cncfcompt.bcn	$⊢ φ \to (x \in A ⟼ B) : A \underset{cn}{⟶} C$
2		cncfcompt.f	$⊢ φ \to F : C \underset{cn}{⟶} D$
3		cncff	$⊢ F : C \underset{cn}{⟶} D \to F : C ⟶ D$
4	2 3	syl	$⊢ φ \to F : C ⟶ D$
5	4	adantr	$⊢ (φ \land x \in A) \to F : C ⟶ D$
6		cncff	$⊢ (x \in A ⟼ B) : A \underset{cn}{⟶} C \to (x \in A ⟼ B) : A ⟶ C$
7	1 6	syl	$⊢ φ \to (x \in A ⟼ B) : A ⟶ C$
8	7	fvmptelrn	$⊢ (φ \land x \in A) \to B \in C$
9	5 8	ffvelrnd	$⊢ (φ \land x \in A) \to F (B) \in D$
10	9	fmpttd	$⊢ φ \to (x \in A ⟼ F (B)) : A ⟶ D$
11		cncfrss2	$⊢ F : C \underset{cn}{⟶} D \to D \subseteq ℂ$
12	2 11	syl	$⊢ φ \to D \subseteq ℂ$
13		eqidd	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
14	4	feqmptd	$⊢ φ \to F = (y \in C ⟼ F (y))$
15		fveq2	$⊢ y = B \to F (y) = F (B)$
16	8 13 14 15	fmptco	$⊢ φ \to F \circ (x \in A ⟼ B) = (x \in A ⟼ F (B))$
17		ssid	$⊢ ℂ \subseteq ℂ$
18		cncfss	$⊢ (D \subseteq ℂ \land ℂ \subseteq ℂ) \to C \underset{cn}{⟶} D \subseteq C \underset{cn}{⟶} ℂ$
19	12 17 18	sylancl	$⊢ φ \to C \underset{cn}{⟶} D \subseteq C \underset{cn}{⟶} ℂ$
20	19 2	sseldd	$⊢ φ \to F : C \underset{cn}{⟶} ℂ$
21	1 20	cncfco	$⊢ φ \to (F \circ (x \in A ⟼ B)) : A \underset{cn}{⟶} ℂ$
22	16 21	eqeltrrd	$⊢ φ \to (x \in A ⟼ F (B)) : A \underset{cn}{⟶} ℂ$
23		cncffvrn	$⊢ (D \subseteq ℂ \land (x \in A ⟼ F (B)) : A \underset{cn}{⟶} ℂ) \to ((x \in A ⟼ F (B)) : A \underset{cn}{⟶} D \leftrightarrow (x \in A ⟼ F (B)) : A ⟶ D)$
24	12 22 23	syl2anc	$⊢ φ \to ((x \in A ⟼ F (B)) : A \underset{cn}{⟶} D \leftrightarrow (x \in A ⟼ F (B)) : A ⟶ D)$
25	10 24	mpbird	$⊢ φ \to (x \in A ⟼ F (B)) : A \underset{cn}{⟶} D$

Metamath Proof Explorer

Theorem cncfcompt

Proof