Theorem cnmpt12

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptid.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt11.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
	cnmpt1t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) )
	cnmpt12.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt12.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
	cnmpt12.c	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑀 ) )
	cnmpt12.d	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐶 = 𝐷 )
Assertion	cnmpt12	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) ∈ ( 𝐽 Cn 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt11.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
3		cnmpt1t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) )
4		cnmpt12.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5		cnmpt12.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
6		cnmpt12.c	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑀 ) )
7		cnmpt12.d	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐶 = 𝐷 )
8		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
9	1 4 2 8	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
10	9	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
11		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑍 )
12	1 5 3 11	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑍 )
13	12	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑍 )
14	10 13	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑍 ) )
15		txtopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑍 ) ) )
16	4 5 15	syl2anc	⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑍 ) ) )
17		cntop2	⊢ ( ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑀 ) → 𝑀 ∈ Top )
18	6 17	syl	⊢ ( 𝜑 → 𝑀 ∈ Top )
19		toptopon2	⊢ ( 𝑀 ∈ Top ↔ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
20	18 19	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
21		cnf2	⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑍 ) ) ∧ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) ∧ ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑀 ) ) → ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) : ( 𝑌 × 𝑍 ) ⟶ ∪ 𝑀 )
22	16 20 6 21	syl3anc	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) : ( 𝑌 × 𝑍 ) ⟶ ∪ 𝑀 )
23		eqid	⊢ ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) = ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 )
24	23	fmpo	⊢ ( ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ 𝑍 𝐶 ∈ ∪ 𝑀 ↔ ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) : ( 𝑌 × 𝑍 ) ⟶ ∪ 𝑀 )
25	22 24	sylibr	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ 𝑍 𝐶 ∈ ∪ 𝑀 )
26		r2al	⊢ ( ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ 𝑍 𝐶 ∈ ∪ 𝑀 ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → 𝐶 ∈ ∪ 𝑀 ) )
27	25 26	sylib	⊢ ( 𝜑 → ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → 𝐶 ∈ ∪ 𝑀 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → 𝐶 ∈ ∪ 𝑀 ) )
29		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑌 ↔ 𝐴 ∈ 𝑌 ) )
30		eleq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ 𝑍 ↔ 𝐵 ∈ 𝑍 ) )
31	29 30	bi2anan9	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) ↔ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑍 ) ) )
32	7	eleq1d	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( 𝐶 ∈ ∪ 𝑀 ↔ 𝐷 ∈ ∪ 𝑀 ) )
33	31 32	imbi12d	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → 𝐶 ∈ ∪ 𝑀 ) ↔ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑍 ) → 𝐷 ∈ ∪ 𝑀 ) ) )
34	33	spc2gv	⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑍 ) → ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍 ) → 𝐶 ∈ ∪ 𝑀 ) → ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑍 ) → 𝐷 ∈ ∪ 𝑀 ) ) )
35	14 28 14 34	syl3c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ∪ 𝑀 )
36	7 23	ovmpoga	⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑍 ∧ 𝐷 ∈ ∪ 𝑀 ) → ( 𝐴 ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) 𝐵 ) = 𝐷 )
37	10 13 35 36	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) 𝐵 ) = 𝐷 )
38	37	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
39	1 2 3 6	cnmpt12f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( 𝑦 ∈ 𝑌 , 𝑧 ∈ 𝑍 ↦ 𝐶 ) 𝐵 ) ) ∈ ( 𝐽 Cn 𝑀 ) )
40	38 39	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) ∈ ( 𝐽 Cn 𝑀 ) )