Theorem cnmpt1t

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	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt11.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
	cnmpt1t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) )
Assertion	cnmpt1t	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt11.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
3		cnmpt1t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) )
4		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
5		mpteq1	⊢ ( 𝑋 = ∪ 𝐽 → ( 𝑥 ∈ 𝑋 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) )
6	1 4 5	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
8		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
9	2 8	syl	⊢ ( 𝜑 → 𝐾 ∈ Top )
10		toptopon2	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
11	9 10	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
12		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ 𝐾 )
13	1 11 2 12	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ 𝐾 )
14	13	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ∪ 𝐾 )
15		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
16	15	fvmpt2	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ 𝐾 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
17	7 14 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
18		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) → 𝐿 ∈ Top )
19	3 18	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
20		toptopon2	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
21	19 20	sylib	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
22		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ∪ 𝐿 )
23	1 21 3 22	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ∪ 𝐿 )
24	23	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ∪ 𝐿 )
25		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
26	25	fvmpt2	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐵 ∈ ∪ 𝐿 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
27	7 24 26	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
28	17 27	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
29	28	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
30	6 29	eqtr3d	⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
31		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
32		nfcv	⊢ Ⅎ 𝑦 ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩
33		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑦 )
34		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑦 )
35	33 34	nfop	⊢ Ⅎ 𝑥 ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑦 ) ⟩
36		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑦 ) )
37		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑦 ) )
38	36 37	opeq12d	⊢ ( 𝑥 = 𝑦 → ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑦 ) ⟩ )
39	32 35 38	cbvmpt	⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑦 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑦 ) ⟩ )
40	31 39	txcnmpt	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) ) → ( 𝑥 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )
41	2 3 40	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝐽 ↦ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )
42	30 41	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )