Metamath Proof Explorer

Theorem limccnp2

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses limccnp2.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝑋 )
limccnp2.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ∈ 𝑌 )
limccnp2.x ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
limccnp2.y ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
limccnp2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limccnp2.j ⊢ 𝐽 = ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) )
limccnp2.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝐵 ) )
limccnp2.d ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑆 ) limℂ 𝐵 ) )
limccnp2.h ⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
Assertion limccnp2 ( 𝜑 → ( 𝐶 𝐻 𝐷 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑅 𝐻 𝑆 ) ) limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limccnp2.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝑋 )
2 limccnp2.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ∈ 𝑌 )
3 limccnp2.x ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
4 limccnp2.y ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
5 limccnp2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
6 limccnp2.j ⊢ 𝐽 = ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) )
7 limccnp2.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝐵 ) )
8 limccnp2.d ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑆 ) limℂ 𝐵 ) )
9 limccnp2.h ⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
10 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
11 10 cnprcl ⊢ ( 𝐻 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝐽 )
12 9 11 syl ⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝐽 )
13 5 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
14 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
15 13 13 14 mp2an ⊢ ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
16 xpss12 ⊢ ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) )
17 3 4 16 syl2anc ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) )
18 resttopon ⊢ ( ( ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) ) → ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
19 15 17 18 sylancr ⊢ ( 𝜑 → ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
20 6 19 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
21 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ 𝐽 )
22 20 21 syl ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ∪ 𝐽 )
23 12 22 eleqtrrd ⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) )
24 opelxp ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) )
25 23 24 sylib ⊢ ( 𝜑 → ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) )
26 25 simpld ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝑥 = 𝐵 ) → 𝐶 ∈ 𝑋 )
28 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝜑 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) )
30 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐵 } ) )
31 29 30 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐵 } ) )
32 31 ord ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( ¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝐵 } ) )
33 elsni ⊢ ( 𝑥 ∈ { 𝐵 } → 𝑥 = 𝐵 )
34 32 33 syl6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( ¬ 𝑥 ∈ 𝐴 → 𝑥 = 𝐵 ) )
35 34 con1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( ¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐴 ) )
36 35 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 )
37 28 36 1 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑅 ∈ 𝑋 )
38 27 37 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) ∈ 𝑋 )
39 25 simprd ⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
40 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝑥 = 𝐵 ) → 𝐷 ∈ 𝑌 )
41 28 36 2 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑆 ∈ 𝑌 )
42 40 41 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ∈ 𝑌 )
43 38 42 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
44 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) )
45 13 a1i ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℂ ) )
46 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐻 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐻 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
47 20 45 9 46 syl3anc ⊢ ( 𝜑 → 𝐻 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
48 47 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝐻 ‘ 𝑦 ) ) )
49 fveq2 ⊢ ( 𝑦 = ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) )
50 df-ov ⊢ ( if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) 𝐻 if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ) = ( 𝐻 ‘ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ )
51 ovif12 ⊢ ( if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) 𝐻 if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ) = if ( 𝑥 = 𝐵 , ( 𝐶 𝐻 𝐷 ) , ( 𝑅 𝐻 𝑆 ) )
52 50 51 eqtr3i ⊢ ( 𝐻 ‘ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) = if ( 𝑥 = 𝐵 , ( 𝐶 𝐻 𝐷 ) , ( 𝑅 𝐻 𝑆 ) )
53 49 52 eqtrdi ⊢ ( 𝑦 = ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ → ( 𝐻 ‘ 𝑦 ) = if ( 𝑥 = 𝐵 , ( 𝐶 𝐻 𝐷 ) , ( 𝑅 𝐻 𝑆 ) ) )
54 43 44 48 53 fmptco ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐶 𝐻 𝐷 ) , ( 𝑅 𝐻 𝑆 ) ) ) )
55 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
56 55 1 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = 𝐴 )
57 limcrcl ⊢ ( 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ⟶ ℂ ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
58 7 57 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ⟶ ℂ ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
59 58 simp2d ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ⊆ ℂ )
60 56 59 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
61 58 simp3d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
62 61 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ℂ )
63 60 62 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ )
64 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
65 13 63 64 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
66 ssun2 ⊢ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } )
67 snssg ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
68 61 67 syl ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
69 66 68 mpbiri ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) )
70 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ⊆ ℂ )
71 70 1 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℂ )
72 eqid ⊢ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
73 60 61 71 72 5 limcmpt ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) limℂ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
74 7 73 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
75 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ⊆ ℂ )
76 75 2 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ∈ ℂ )
77 60 61 76 72 5 limcmpt ⊢ ( 𝜑 → ( 𝐷 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝑆 ) limℂ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
78 8 77 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
79 65 45 45 69 74 78 txcnp ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ×t 𝐾 ) ) ‘ 𝐵 ) )
80 15 topontopi ⊢ ( 𝐾 ×t 𝐾 ) ∈ Top
81 80 a1i ⊢ ( 𝜑 → ( 𝐾 ×t 𝐾 ) ∈ Top )
82 43 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ( 𝑋 × 𝑌 ) )
83 toponuni ⊢ ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝐴 ∪ { 𝐵 } ) = ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) )
84 65 83 syl ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) = ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) )
85 84 feq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ( 𝑋 × 𝑌 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) : ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ⟶ ( 𝑋 × 𝑌 ) ) )
86 82 85 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) : ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ⟶ ( 𝑋 × 𝑌 ) )
87 eqid ⊢ ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
88 15 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( 𝐾 ×t 𝐾 )
89 87 88 cnprest2 ⊢ ( ( ( 𝐾 ×t 𝐾 ) ∈ Top ∧ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) : ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) ) → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ×t 𝐾 ) ) ‘ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) ) ‘ 𝐵 ) ) )
90 81 86 17 89 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ×t 𝐾 ) ) ‘ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) ) ‘ 𝐵 ) ) )
91 79 90 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) ) ‘ 𝐵 ) )
92 6 oveq2i ⊢ ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) = ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) )
93 92 fveq1i ⊢ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) ‘ 𝐵 ) = ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( ( 𝐾 ×t 𝐾 ) ↾t ( 𝑋 × 𝑌 ) ) ) ‘ 𝐵 )
94 91 93 eleqtrrdi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) ‘ 𝐵 ) )
95 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) = 𝐶 )
96 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) = 𝐷 )
97 95 96 opeq12d ⊢ ( 𝑥 = 𝐵 → ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
98 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ )
99 opex ⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
100 97 98 99 fvmpt ⊢ ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ‘ 𝐵 ) = ⟨ 𝐶 , 𝐷 ⟩ )
101 69 100 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ‘ 𝐵 ) = ⟨ 𝐶 , 𝐷 ⟩ )
102 101 fveq2d ⊢ ( 𝜑 → ( ( 𝐽 CnP 𝐾 ) ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ‘ 𝐵 ) ) = ( ( 𝐽 CnP 𝐾 ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
103 9 102 eleqtrrd ⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ‘ 𝐵 ) ) )
104 cnpco ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) ‘ 𝐵 ) ∧ 𝐻 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ‘ 𝐵 ) ) ) → ( 𝐻 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
105 94 103 104 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ⟨ if ( 𝑥 = 𝐵 , 𝐶 , 𝑅 ) , if ( 𝑥 = 𝐵 , 𝐷 , 𝑆 ) ⟩ ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
106 54 105 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐶 𝐻 𝐷 ) , ( 𝑅 𝐻 𝑆 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
107 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
108 107 1 2 fovrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 𝐻 𝑆 ) ∈ ℂ )
109 60 61 108 72 5 limcmpt ⊢ ( 𝜑 → ( ( 𝐶 𝐻 𝐷 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑅 𝐻 𝑆 ) ) limℂ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐶 𝐻 𝐷 ) , ( 𝑅 𝐻 𝑆 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
110 106 109 mpbird ⊢ ( 𝜑 → ( 𝐶 𝐻 𝐷 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑅 𝐻 𝑆 ) ) limℂ 𝐵 ) )