Theorem cnmpt22

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	cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
	cnmpt2t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
	cnmpt22.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
	cnmpt22.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
	cnmpt22.c	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
	cnmpt22.d	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝐶 = 𝐷 )
Assertion	cnmpt22	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐷 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4		cnmpt2t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
5		cnmpt22.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
6		cnmpt22.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
7		cnmpt22.c	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
8		cnmpt22.d	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → 𝐶 = 𝐷 )
9		df-ov	⊢ ( 𝐴 ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) 𝐵 ) = ( ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
10		txtopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11	1 2 10	syl2anc	⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
12		cnf2	⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
13	11 5 3 12	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
14		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
15	14	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
16	13 15	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 )
17		rsp2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑍 ) )
18	16 17	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑍 ) )
19	18	3impib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑍 )
20		cnf2	⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑊 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑊 )
21	11 6 4 20	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑊 )
22		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
23	22	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ 𝑊 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑊 )
24	21 23	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ 𝑊 )
25		rsp2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ 𝑊 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ 𝑊 ) )
26	24 25	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ 𝑊 ) )
27	26	3impib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ 𝑊 )
28	19 27	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑊 ) )
29		txtopon	⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑊 ) ) → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑍 × 𝑊 ) ) )
30	5 6 29	syl2anc	⊢ ( 𝜑 → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑍 × 𝑊 ) ) )
31		cntop2	⊢ ( ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) → 𝑁 ∈ Top )
32	7 31	syl	⊢ ( 𝜑 → 𝑁 ∈ Top )
33		toptopon2	⊢ ( 𝑁 ∈ Top ↔ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
34	32 33	sylib	⊢ ( 𝜑 → 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
35		cnf2	⊢ ( ( ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑍 × 𝑊 ) ) ∧ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) ∧ ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) ) → ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) : ( 𝑍 × 𝑊 ) ⟶ ∪ 𝑁 )
36	30 34 7 35	syl3anc	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) : ( 𝑍 × 𝑊 ) ⟶ ∪ 𝑁 )
37		eqid	⊢ ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) = ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 )
38	37	fmpo	⊢ ( ∀ 𝑧 ∈ 𝑍 ∀ 𝑤 ∈ 𝑊 𝐶 ∈ ∪ 𝑁 ↔ ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) : ( 𝑍 × 𝑊 ) ⟶ ∪ 𝑁 )
39	36 38	sylibr	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑍 ∀ 𝑤 ∈ 𝑊 𝐶 ∈ ∪ 𝑁 )
40		r2al	⊢ ( ∀ 𝑧 ∈ 𝑍 ∀ 𝑤 ∈ 𝑊 𝐶 ∈ ∪ 𝑁 ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑍 ∧ 𝑤 ∈ 𝑊 ) → 𝐶 ∈ ∪ 𝑁 ) )
41	39 40	sylib	⊢ ( 𝜑 → ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑍 ∧ 𝑤 ∈ 𝑊 ) → 𝐶 ∈ ∪ 𝑁 ) )
42	41	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑍 ∧ 𝑤 ∈ 𝑊 ) → 𝐶 ∈ ∪ 𝑁 ) )
43		eleq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ∈ 𝑍 ↔ 𝐴 ∈ 𝑍 ) )
44		eleq1	⊢ ( 𝑤 = 𝐵 → ( 𝑤 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) )
45	43 44	bi2anan9	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ( ( 𝑧 ∈ 𝑍 ∧ 𝑤 ∈ 𝑊 ) ↔ ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑊 ) ) )
46	8	eleq1d	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ( 𝐶 ∈ ∪ 𝑁 ↔ 𝐷 ∈ ∪ 𝑁 ) )
47	45 46	imbi12d	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ( ( ( 𝑧 ∈ 𝑍 ∧ 𝑤 ∈ 𝑊 ) → 𝐶 ∈ ∪ 𝑁 ) ↔ ( ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑊 ) → 𝐷 ∈ ∪ 𝑁 ) ) )
48	47	spc2gv	⊢ ( ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑍 ∧ 𝑤 ∈ 𝑊 ) → 𝐶 ∈ ∪ 𝑁 ) → ( ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑊 ) → 𝐷 ∈ ∪ 𝑁 ) ) )
49	28 42 28 48	syl3c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐷 ∈ ∪ 𝑁 )
50	8 37	ovmpoga	⊢ ( ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑊 ∧ 𝐷 ∈ ∪ 𝑁 ) → ( 𝐴 ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) 𝐵 ) = 𝐷 )
51	19 27 49 50	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) 𝐵 ) = 𝐷 )
52	9 51	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐷 )
53	52	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐷 ) )
54	1 2 3 4	cnmpt2t	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐿 ×t 𝑀 ) ) )
55	1 2 54 7	cnmpt21f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ∈ 𝑍 , 𝑤 ∈ 𝑊 ↦ 𝐶 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )
56	53 55	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐷 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )