Metamath Proof Explorer

Theorem cnmpt11

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 𝐾 ) )
cnmpt11.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
cnmpt11.b ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐿 ) )
cnmpt11.c ⊢ ( 𝑦 = 𝐴 → 𝐵 = 𝐶 )
Assertion cnmpt11 ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ∈ ( 𝐽 Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnmptid.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmpt11.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
3 cnmpt11.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
4 cnmpt11.b ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐿 ) )
5 cnmpt11.c ⊢ ( 𝑦 = 𝐴 → 𝐵 = 𝐶 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
7 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
8 1 3 2 7 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
9 8 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
10 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
11 10 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
12 6 9 11 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
13 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝐴 ) )
14 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐵 )
15 5 eleq1d ⊢ ( 𝑦 = 𝐴 → ( 𝐵 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿 ) )
16 cntop2 ⊢ ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐿 ) → 𝐿 ∈ Top )
17 4 16 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
18 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
19 17 18 sylib ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
20 cnf2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) : 𝑌 ⟶ ∪ 𝐿 )
21 3 19 4 20 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) : 𝑌 ⟶ ∪ 𝐿 )
22 14 fmpt ⊢ ( ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿 ↔ ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) : 𝑌 ⟶ ∪ 𝐿 )
23 21 22 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝐿 )
25 15 24 9 rspcdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ∪ 𝐿 )
26 14 5 9 25 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 )
27 13 26 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = 𝐶 )
28 fvco3 ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) )
29 8 28 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) )
30 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 )
31 30 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐶 ∈ ∪ 𝐿 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
32 6 25 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
33 27 29 32 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) )
34 33 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) )
35 nfv ⊢ Ⅎ 𝑧 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 )
36 nfcv ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑌 ↦ 𝐵 )
37 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
38 36 37 nfco ⊢ Ⅎ 𝑥 ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
39 nfcv ⊢ Ⅎ 𝑥 𝑧
40 38 39 nffv ⊢ Ⅎ 𝑥 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 )
41 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ 𝐶 )
42 41 39 nffv ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 )
43 40 42 nfeq ⊢ Ⅎ 𝑥 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 )
44 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) )
45 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 ) )
46 44 45 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) ↔ ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 ) ) )
47 35 43 46 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 ) )
48 34 47 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 ) )
49 fco ⊢ ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) : 𝑌 ⟶ ∪ 𝐿 ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐿 )
50 21 8 49 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐿 )
51 50 ffnd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) Fn 𝑋 )
52 25 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) : 𝑋 ⟶ ∪ 𝐿 )
53 52 ffnd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) Fn 𝑋 )
54 eqfnfv ⊢ ( ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) Fn 𝑋 ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) Fn 𝑋 ) → ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 ) ) )
55 51 53 54 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ‘ 𝑧 ) ) )
56 48 55 mpbird ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
57 cnco ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
58 2 4 57 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
59 56 58 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ∈ ( 𝐽 Cn 𝐿 ) )