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