cncfmpt2f

Description: Composition of continuous functions. -cn-> analogue of cnmpt12f . (Contributed by Mario Carneiro, 3-Sep-2014)

Step	Hyp	Ref	Expression
1		cncfmpt2f.1	$⊢ J = TopOpen (ℂ_{fld})$
2		cncfmpt2f.2	$⊢ φ \to F \in ((J \times_{t} J) Cn J)$
3		cncfmpt2f.3	$⊢ φ \to (x \in X ⟼ A) : X \underset{cn}{⟶} ℂ$
4		cncfmpt2f.4	$⊢ φ \to (x \in X ⟼ B) : X \underset{cn}{⟶} ℂ$
5	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
6		cncfrss	$⊢ (x \in X ⟼ A) : X \underset{cn}{⟶} ℂ \to X \subseteq ℂ$
7	3 6	syl	$⊢ φ \to X \subseteq ℂ$
8		resttopon	$⊢ (J \in TopOn (ℂ) \land X \subseteq ℂ) \to J ↾_{𝑡} X \in TopOn (X)$
9	5 7 8	sylancr	$⊢ φ \to J ↾_{𝑡} X \in TopOn (X)$
10		ssid	$⊢ ℂ \subseteq ℂ$
11		eqid	$⊢ J ↾_{𝑡} X = J ↾_{𝑡} X$
12	5	toponrestid	$⊢ J = J ↾_{𝑡} ℂ$
13	1 11 12	cncfcn	$⊢ (X \subseteq ℂ \land ℂ \subseteq ℂ) \to X \underset{cn}{⟶} ℂ = (J ↾_{𝑡} X) Cn J$
14	7 10 13	sylancl	$⊢ φ \to X \underset{cn}{⟶} ℂ = (J ↾_{𝑡} X) Cn J$
15	3 14	eleqtrd	$⊢ φ \to (x \in X ⟼ A) \in ((J ↾_{𝑡} X) Cn J)$
16	4 14	eleqtrd	$⊢ φ \to (x \in X ⟼ B) \in ((J ↾_{𝑡} X) Cn J)$
17	9 15 16 2	cnmpt12f	$⊢ φ \to (x \in X ⟼ A F B) \in ((J ↾_{𝑡} X) Cn J)$
18	17 14	eleqtrrd	$⊢ φ \to (x \in X ⟼ A F B) : X \underset{cn}{⟶} ℂ$

Metamath Proof Explorer