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

Metamath Proof Explorer

Theorem cnmpt22f

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 𝑀 ) )
cnmpt22f.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
Assertion cnmpt22f ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ×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 cnmpt22f.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
6 cntop2 ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) → 𝐿 ∈ Top )
7 3 6 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
8 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
9 7 8 sylib ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
10 cntop2 ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) → 𝑀 ∈ Top )
11 4 10 syl ⊢ ( 𝜑 → 𝑀 ∈ Top )
12 toptopon2 ⊢ ( 𝑀 ∈ Top ↔ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
13 11 12 sylib ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
14 txtopon ⊢ ( ( 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) ) → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( ∪ 𝐿 × ∪ 𝑀 ) ) )
15 9 13 14 syl2anc ⊢ ( 𝜑 → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( ∪ 𝐿 × ∪ 𝑀 ) ) )
16 cntop2 ⊢ ( 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) → 𝑁 ∈ Top )
17 5 16 syl ⊢ ( 𝜑 → 𝑁 ∈ Top )
18 toptopon2 ⊢ ( 𝑁 ∈ Top ↔ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
19 17 18 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
20 cnf2 ⊢ ( ( ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( ∪ 𝐿 × ∪ 𝑀 ) ) ∧ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) ∧ 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) ) → 𝐹 : ( ∪ 𝐿 × ∪ 𝑀 ) ⟶ ∪ 𝑁 )
21 15 19 5 20 syl3anc ⊢ ( 𝜑 → 𝐹 : ( ∪ 𝐿 × ∪ 𝑀 ) ⟶ ∪ 𝑁 )
22 21 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( ∪ 𝐿 × ∪ 𝑀 ) )
23 fnov ⊢ ( 𝐹 Fn ( ∪ 𝐿 × ∪ 𝑀 ) ↔ 𝐹 = ( 𝑧 ∈ ∪ 𝐿 , 𝑤 ∈ ∪ 𝑀 ↦ ( 𝑧 𝐹 𝑤 ) ) )
24 22 23 sylib ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ∪ 𝐿 , 𝑤 ∈ ∪ 𝑀 ↦ ( 𝑧 𝐹 𝑤 ) ) )
25 24 5 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐿 , 𝑤 ∈ ∪ 𝑀 ↦ ( 𝑧 𝐹 𝑤 ) ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
26 oveq12 ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ( 𝑧 𝐹 𝑤 ) = ( 𝐴 𝐹 𝐵 ) )
27 1 2 3 4 9 13 25 26 cnmpt22 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )