This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) )