Metamath Proof Explorer

Theorem cxpcn3

Description: Extend continuity of the complex power function to a base of zero, as long as the exponent has strictly positive real part. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses cxpcn3.d ⊢ 𝐷 = ( ◡ ℜ “ ℝ+ )
cxpcn3.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cxpcn3.k ⊢ 𝐾 = ( 𝐽 ↾t ( 0 [,) +∞ ) )
cxpcn3.l ⊢ 𝐿 = ( 𝐽 ↾t 𝐷 )
Assertion cxpcn3 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 cxpcn3.d ⊢ 𝐷 = ( ◡ ℜ “ ℝ+ )
2 cxpcn3.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
3 cxpcn3.k ⊢ 𝐾 = ( 𝐽 ↾t ( 0 [,) +∞ ) )
4 cxpcn3.l ⊢ 𝐿 = ( 𝐽 ↾t 𝐷 )
5 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
6 ax-resscn ⊢ ℝ ⊆ ℂ
7 5 6 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
8 7 sseli ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℂ )
9 cnvimass ⊢ ( ◡ ℜ “ ℝ+ ) ⊆ dom ℜ
10 ref ⊢ ℜ : ℂ ⟶ ℝ
11 10 fdmi ⊢ dom ℜ = ℂ
12 9 11 sseqtri ⊢ ( ◡ ℜ “ ℝ+ ) ⊆ ℂ
13 1 12 eqsstri ⊢ 𝐷 ⊆ ℂ
14 13 sseli ⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ ℂ )
15 cxpcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ↑𝑐 𝑦 ) ∈ ℂ )
16 8 14 15 syl2an ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 𝑦 ) ∈ ℂ )
17 16 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,) +∞ ) ∀ 𝑦 ∈ 𝐷 ( 𝑥 ↑𝑐 𝑦 ) ∈ ℂ
18 eqid ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) )
19 18 fmpo ⊢ ( ∀ 𝑥 ∈ ( 0 [,) +∞ ) ∀ 𝑦 ∈ 𝐷 ( 𝑥 ↑𝑐 𝑦 ) ∈ ℂ ↔ ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ )
20 17 19 mpbi ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ
21 2 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
22 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
23 rpge0 ⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ 𝑥 )
24 elrege0 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
25 22 23 24 sylanbrc ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ( 0 [,) +∞ ) )
26 25 ssriv ⊢ ℝ+ ⊆ ( 0 [,) +∞ )
27 26 7 sstri ⊢ ℝ+ ⊆ ℂ
28 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ℝ+ ⊆ ℂ ) → ( 𝐽 ↾t ℝ+ ) ∈ ( TopOn ‘ ℝ+ ) )
29 21 27 28 mp2an ⊢ ( 𝐽 ↾t ℝ+ ) ∈ ( TopOn ‘ ℝ+ )
30 29 toponrestid ⊢ ( 𝐽 ↾t ℝ+ ) = ( ( 𝐽 ↾t ℝ+ ) ↾t ℝ+ )
31 29 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝐽 ↾t ℝ+ ) ∈ ( TopOn ‘ ℝ+ ) )
32 ssid ⊢ ℝ+ ⊆ ℝ+
33 32 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ℝ+ ⊆ ℝ+ )
34 21 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
35 13 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → 𝐷 ⊆ ℂ )
36 eqid ⊢ ( 𝐽 ↾t ℝ+ ) = ( 𝐽 ↾t ℝ+ )
37 2 36 cxpcn2 ⊢ ( 𝑥 ∈ ℝ+ , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐽 ) Cn 𝐽 )
38 37 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝑥 ∈ ℝ+ , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐽 ) Cn 𝐽 ) )
39 30 31 33 4 34 35 38 cnmpt2res ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝑥 ∈ ℝ+ , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) Cn 𝐽 ) )
40 elrege0 ⊢ ( 𝑢 ∈ ( 0 [,) +∞ ) ↔ ( 𝑢 ∈ ℝ ∧ 0 ≤ 𝑢 ) )
41 40 simplbi ⊢ ( 𝑢 ∈ ( 0 [,) +∞ ) → 𝑢 ∈ ℝ )
42 41 adantr ⊢ ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) → 𝑢 ∈ ℝ )
43 42 adantr ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → 𝑢 ∈ ℝ )
44 simpr ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → 0 < 𝑢 )
45 43 44 elrpd ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → 𝑢 ∈ ℝ+ )
46 simplr ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → 𝑣 ∈ 𝐷 )
47 45 46 opelxpd ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ℝ+ × 𝐷 ) )
48 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
49 21 13 48 mp2an ⊢ ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 )
50 4 49 eqeltri ⊢ 𝐿 ∈ ( TopOn ‘ 𝐷 )
51 txtopon ⊢ ( ( ( 𝐽 ↾t ℝ+ ) ∈ ( TopOn ‘ ℝ+ ) ∧ 𝐿 ∈ ( TopOn ‘ 𝐷 ) ) → ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) ∈ ( TopOn ‘ ( ℝ+ × 𝐷 ) ) )
52 29 50 51 mp2an ⊢ ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) ∈ ( TopOn ‘ ( ℝ+ × 𝐷 ) )
53 52 toponunii ⊢ ( ℝ+ × 𝐷 ) = ∪ ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 )
54 53 cncnpi ⊢ ( ( ( 𝑥 ∈ ℝ+ , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) Cn 𝐽 ) ∧ ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ℝ+ × 𝐷 ) ) → ( 𝑥 ∈ ℝ+ , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
55 39 47 54 syl2anc ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝑥 ∈ ℝ+ , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
56 ssid ⊢ 𝐷 ⊆ 𝐷
57 resmpo ⊢ ( ( ℝ+ ⊆ ( 0 [,) +∞ ) ∧ 𝐷 ⊆ 𝐷 ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ↾ ( ℝ+ × 𝐷 ) ) = ( 𝑥 ∈ ℝ+ , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) )
58 26 56 57 mp2an ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ↾ ( ℝ+ × 𝐷 ) ) = ( 𝑥 ∈ ℝ+ , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) )
59 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → ( 𝐽 ↾t ( 0 [,) +∞ ) ) ∈ ( TopOn ‘ ( 0 [,) +∞ ) ) )
60 21 7 59 mp2an ⊢ ( 𝐽 ↾t ( 0 [,) +∞ ) ) ∈ ( TopOn ‘ ( 0 [,) +∞ ) )
61 3 60 eqeltri ⊢ 𝐾 ∈ ( TopOn ‘ ( 0 [,) +∞ ) )
62 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
63 iooretop ⊢ ( 0 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
64 62 63 eqeltrri ⊢ ℝ+ ∈ ( topGen ‘ ran (,) )
65 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
66 ovex ⊢ ( 0 [,) +∞ ) ∈ V
67 restopnb ⊢ ( ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 0 [,) +∞ ) ∈ V ) ∧ ( ℝ+ ∈ ( topGen ‘ ran (,) ) ∧ ℝ+ ⊆ ( 0 [,) +∞ ) ∧ ℝ+ ⊆ ℝ+ ) ) → ( ℝ+ ∈ ( topGen ‘ ran (,) ) ↔ ℝ+ ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) ) ) )
68 65 66 67 mpanl12 ⊢ ( ( ℝ+ ∈ ( topGen ‘ ran (,) ) ∧ ℝ+ ⊆ ( 0 [,) +∞ ) ∧ ℝ+ ⊆ ℝ+ ) → ( ℝ+ ∈ ( topGen ‘ ran (,) ) ↔ ℝ+ ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) ) ) )
69 64 26 32 68 mp3an ⊢ ( ℝ+ ∈ ( topGen ‘ ran (,) ) ↔ ℝ+ ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) ) )
70 64 69 mpbi ⊢ ℝ+ ∈ ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) )
71 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
72 2 71 rerest ⊢ ( ( 0 [,) +∞ ) ⊆ ℝ → ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) ) )
73 5 72 ax-mp ⊢ ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) )
74 3 73 eqtri ⊢ 𝐾 = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,) +∞ ) )
75 70 74 eleqtrri ⊢ ℝ+ ∈ 𝐾
76 toponmax ⊢ ( 𝐿 ∈ ( TopOn ‘ 𝐷 ) → 𝐷 ∈ 𝐿 )
77 50 76 ax-mp ⊢ 𝐷 ∈ 𝐿
78 txrest ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ ( 0 [,) +∞ ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝐷 ) ) ∧ ( ℝ+ ∈ 𝐾 ∧ 𝐷 ∈ 𝐿 ) ) → ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) = ( ( 𝐾 ↾t ℝ+ ) ×t ( 𝐿 ↾t 𝐷 ) ) )
79 61 50 75 77 78 mp4an ⊢ ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) = ( ( 𝐾 ↾t ℝ+ ) ×t ( 𝐿 ↾t 𝐷 ) )
80 3 oveq1i ⊢ ( 𝐾 ↾t ℝ+ ) = ( ( 𝐽 ↾t ( 0 [,) +∞ ) ) ↾t ℝ+ )
81 restabs ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ℝ+ ⊆ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ∈ V ) → ( ( 𝐽 ↾t ( 0 [,) +∞ ) ) ↾t ℝ+ ) = ( 𝐽 ↾t ℝ+ ) )
82 21 26 66 81 mp3an ⊢ ( ( 𝐽 ↾t ( 0 [,) +∞ ) ) ↾t ℝ+ ) = ( 𝐽 ↾t ℝ+ )
83 80 82 eqtri ⊢ ( 𝐾 ↾t ℝ+ ) = ( 𝐽 ↾t ℝ+ )
84 50 toponunii ⊢ 𝐷 = ∪ 𝐿
85 84 restid ⊢ ( 𝐿 ∈ ( TopOn ‘ 𝐷 ) → ( 𝐿 ↾t 𝐷 ) = 𝐿 )
86 50 85 ax-mp ⊢ ( 𝐿 ↾t 𝐷 ) = 𝐿
87 83 86 oveq12i ⊢ ( ( 𝐾 ↾t ℝ+ ) ×t ( 𝐿 ↾t 𝐷 ) ) = ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 )
88 79 87 eqtri ⊢ ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) = ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 )
89 88 oveq1i ⊢ ( ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) CnP 𝐽 ) = ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) CnP 𝐽 )
90 89 fveq1i ⊢ ( ( ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( ( ( 𝐽 ↾t ℝ+ ) ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
91 55 58 90 3eltr4g ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ↾ ( ℝ+ × 𝐷 ) ) ∈ ( ( ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
92 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ( 0 [,) +∞ ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝐷 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( ( 0 [,) +∞ ) × 𝐷 ) ) )
93 61 50 92 mp2an ⊢ ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( ( 0 [,) +∞ ) × 𝐷 ) )
94 93 topontopi ⊢ ( 𝐾 ×t 𝐿 ) ∈ Top
95 94 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝐾 ×t 𝐿 ) ∈ Top )
96 xpss1 ⊢ ( ℝ+ ⊆ ( 0 [,) +∞ ) → ( ℝ+ × 𝐷 ) ⊆ ( ( 0 [,) +∞ ) × 𝐷 ) )
97 26 96 mp1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( ℝ+ × 𝐷 ) ⊆ ( ( 0 [,) +∞ ) × 𝐷 ) )
98 txopn ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ ( 0 [,) +∞ ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝐷 ) ) ∧ ( ℝ+ ∈ 𝐾 ∧ 𝐷 ∈ 𝐿 ) ) → ( ℝ+ × 𝐷 ) ∈ ( 𝐾 ×t 𝐿 ) )
99 61 50 75 77 98 mp4an ⊢ ( ℝ+ × 𝐷 ) ∈ ( 𝐾 ×t 𝐿 )
100 isopn3i ⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ Top ∧ ( ℝ+ × 𝐷 ) ∈ ( 𝐾 ×t 𝐿 ) ) → ( ( int ‘ ( 𝐾 ×t 𝐿 ) ) ‘ ( ℝ+ × 𝐷 ) ) = ( ℝ+ × 𝐷 ) )
101 94 99 100 mp2an ⊢ ( ( int ‘ ( 𝐾 ×t 𝐿 ) ) ‘ ( ℝ+ × 𝐷 ) ) = ( ℝ+ × 𝐷 )
102 47 101 eleqtrrdi ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ( int ‘ ( 𝐾 ×t 𝐿 ) ) ‘ ( ℝ+ × 𝐷 ) ) )
103 20 a1i ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ )
104 61 topontopi ⊢ 𝐾 ∈ Top
105 50 topontopi ⊢ 𝐿 ∈ Top
106 61 toponunii ⊢ ( 0 [,) +∞ ) = ∪ 𝐾
107 104 105 106 84 txunii ⊢ ( ( 0 [,) +∞ ) × 𝐷 ) = ∪ ( 𝐾 ×t 𝐿 )
108 21 toponunii ⊢ ℂ = ∪ 𝐽
109 107 108 cnprest ⊢ ( ( ( ( 𝐾 ×t 𝐿 ) ∈ Top ∧ ( ℝ+ × 𝐷 ) ⊆ ( ( 0 [,) +∞ ) × 𝐷 ) ) ∧ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ( int ‘ ( 𝐾 ×t 𝐿 ) ) ‘ ( ℝ+ × 𝐷 ) ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ ) ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ↔ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ↾ ( ℝ+ × 𝐷 ) ) ∈ ( ( ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
110 95 97 102 103 109 syl22anc ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ↔ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ↾ ( ℝ+ × 𝐷 ) ) ∈ ( ( ( ( 𝐾 ×t 𝐿 ) ↾t ( ℝ+ × 𝐷 ) ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
111 91 110 mpbird ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 < 𝑢 ) → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
112 20 a1i ⊢ ( 𝑣 ∈ 𝐷 → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ )
113 eqid ⊢ ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) = ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 )
114 eqid ⊢ if ( ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) ≤ ( 𝑒 ↑𝑐 ( 1 / ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) ) ) , ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) , ( 𝑒 ↑𝑐 ( 1 / ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) ) ) ) = if ( ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) ≤ ( 𝑒 ↑𝑐 ( 1 / ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) ) ) , ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) , ( 𝑒 ↑𝑐 ( 1 / ( if ( ( ℜ ‘ 𝑣 ) ≤ 1 , ( ℜ ‘ 𝑣 ) , 1 ) / 2 ) ) ) )
115 1 2 3 4 113 114 cxpcn3lem ⊢ ( ( 𝑣 ∈ 𝐷 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) )
116 115 ralrimiva ⊢ ( 𝑣 ∈ 𝐷 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) )
117 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
118 117 a1i ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 0 ∈ ( 0 [,) +∞ ) )
119 simprl ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑎 ∈ ( 0 [,) +∞ ) )
120 118 119 ovresd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) = ( 0 ( abs ∘ − ) 𝑎 ) )
121 0cn ⊢ 0 ∈ ℂ
122 7 119 sselid ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑎 ∈ ℂ )
123 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
124 123 cnmetdval ⊢ ( ( 0 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 0 ( abs ∘ − ) 𝑎 ) = ( abs ‘ ( 0 − 𝑎 ) ) )
125 121 122 124 sylancr ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ( abs ∘ − ) 𝑎 ) = ( abs ‘ ( 0 − 𝑎 ) ) )
126 df-neg ⊢ - 𝑎 = ( 0 − 𝑎 )
127 126 fveq2i ⊢ ( abs ‘ - 𝑎 ) = ( abs ‘ ( 0 − 𝑎 ) )
128 122 absnegd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( abs ‘ - 𝑎 ) = ( abs ‘ 𝑎 ) )
129 127 128 eqtr3id ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( abs ‘ ( 0 − 𝑎 ) ) = ( abs ‘ 𝑎 ) )
130 120 125 129 3eqtrd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) = ( abs ‘ 𝑎 ) )
131 130 breq1d ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ↔ ( abs ‘ 𝑎 ) < 𝑑 ) )
132 simpl ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑣 ∈ 𝐷 )
133 simprr ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑏 ∈ 𝐷 )
134 132 133 ovresd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) = ( 𝑣 ( abs ∘ − ) 𝑏 ) )
135 13 132 sselid ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑣 ∈ ℂ )
136 13 133 sselid ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑏 ∈ ℂ )
137 123 cnmetdval ⊢ ( ( 𝑣 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑣 ( abs ∘ − ) 𝑏 ) = ( abs ‘ ( 𝑣 − 𝑏 ) ) )
138 135 136 137 syl2anc ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑣 ( abs ∘ − ) 𝑏 ) = ( abs ‘ ( 𝑣 − 𝑏 ) ) )
139 134 138 eqtrd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) = ( abs ‘ ( 𝑣 − 𝑏 ) ) )
140 139 breq1d ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ↔ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) )
141 131 140 anbi12d ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) ↔ ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) ) )
142 oveq12 ⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 𝑣 ) → ( 𝑥 ↑𝑐 𝑦 ) = ( 0 ↑𝑐 𝑣 ) )
143 ovex ⊢ ( 0 ↑𝑐 𝑣 ) ∈ V
144 142 18 143 ovmpoa ⊢ ( ( 0 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) → ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) = ( 0 ↑𝑐 𝑣 ) )
145 117 132 144 sylancr ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) = ( 0 ↑𝑐 𝑣 ) )
146 1 eleq2i ⊢ ( 𝑣 ∈ 𝐷 ↔ 𝑣 ∈ ( ◡ ℜ “ ℝ+ ) )
147 ffn ⊢ ( ℜ : ℂ ⟶ ℝ → ℜ Fn ℂ )
148 elpreima ⊢ ( ℜ Fn ℂ → ( 𝑣 ∈ ( ◡ ℜ “ ℝ+ ) ↔ ( 𝑣 ∈ ℂ ∧ ( ℜ ‘ 𝑣 ) ∈ ℝ+ ) ) )
149 10 147 148 mp2b ⊢ ( 𝑣 ∈ ( ◡ ℜ “ ℝ+ ) ↔ ( 𝑣 ∈ ℂ ∧ ( ℜ ‘ 𝑣 ) ∈ ℝ+ ) )
150 146 149 bitri ⊢ ( 𝑣 ∈ 𝐷 ↔ ( 𝑣 ∈ ℂ ∧ ( ℜ ‘ 𝑣 ) ∈ ℝ+ ) )
151 150 simplbi ⊢ ( 𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ )
152 150 simprbi ⊢ ( 𝑣 ∈ 𝐷 → ( ℜ ‘ 𝑣 ) ∈ ℝ+ )
153 152 rpne0d ⊢ ( 𝑣 ∈ 𝐷 → ( ℜ ‘ 𝑣 ) ≠ 0 )
154 fveq2 ⊢ ( 𝑣 = 0 → ( ℜ ‘ 𝑣 ) = ( ℜ ‘ 0 ) )
155 re0 ⊢ ( ℜ ‘ 0 ) = 0
156 154 155 eqtrdi ⊢ ( 𝑣 = 0 → ( ℜ ‘ 𝑣 ) = 0 )
157 156 necon3i ⊢ ( ( ℜ ‘ 𝑣 ) ≠ 0 → 𝑣 ≠ 0 )
158 153 157 syl ⊢ ( 𝑣 ∈ 𝐷 → 𝑣 ≠ 0 )
159 151 158 0cxpd ⊢ ( 𝑣 ∈ 𝐷 → ( 0 ↑𝑐 𝑣 ) = 0 )
160 159 adantr ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ↑𝑐 𝑣 ) = 0 )
161 145 160 eqtrd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) = 0 )
162 oveq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 ↑𝑐 𝑦 ) = ( 𝑎 ↑𝑐 𝑏 ) )
163 ovex ⊢ ( 𝑎 ↑𝑐 𝑏 ) ∈ V
164 162 18 163 ovmpoa ⊢ ( ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) → ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) = ( 𝑎 ↑𝑐 𝑏 ) )
165 164 adantl ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) = ( 𝑎 ↑𝑐 𝑏 ) )
166 161 165 oveq12d ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) = ( 0 ( abs ∘ − ) ( 𝑎 ↑𝑐 𝑏 ) ) )
167 122 136 cxpcld ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 ↑𝑐 𝑏 ) ∈ ℂ )
168 123 cnmetdval ⊢ ( ( 0 ∈ ℂ ∧ ( 𝑎 ↑𝑐 𝑏 ) ∈ ℂ ) → ( 0 ( abs ∘ − ) ( 𝑎 ↑𝑐 𝑏 ) ) = ( abs ‘ ( 0 − ( 𝑎 ↑𝑐 𝑏 ) ) ) )
169 121 167 168 sylancr ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 0 ( abs ∘ − ) ( 𝑎 ↑𝑐 𝑏 ) ) = ( abs ‘ ( 0 − ( 𝑎 ↑𝑐 𝑏 ) ) ) )
170 df-neg ⊢ - ( 𝑎 ↑𝑐 𝑏 ) = ( 0 − ( 𝑎 ↑𝑐 𝑏 ) )
171 170 fveq2i ⊢ ( abs ‘ - ( 𝑎 ↑𝑐 𝑏 ) ) = ( abs ‘ ( 0 − ( 𝑎 ↑𝑐 𝑏 ) ) )
172 167 absnegd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( abs ‘ - ( 𝑎 ↑𝑐 𝑏 ) ) = ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) )
173 171 172 eqtr3id ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( abs ‘ ( 0 − ( 𝑎 ↑𝑐 𝑏 ) ) ) = ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) )
174 166 169 173 3eqtrd ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) = ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) )
175 174 breq1d ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ↔ ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) )
176 141 175 imbi12d ⊢ ( ( 𝑣 ∈ 𝐷 ∧ ( 𝑎 ∈ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) ↔ ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) ) )
177 176 2ralbidva ⊢ ( 𝑣 ∈ 𝐷 → ( ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) ↔ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) ) )
178 177 rexbidv ⊢ ( 𝑣 ∈ 𝐷 → ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) ↔ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) ) )
179 178 ralbidv ⊢ ( 𝑣 ∈ 𝐷 → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝑣 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝑒 ) ) )
180 116 179 mpbird ⊢ ( 𝑣 ∈ 𝐷 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) )
181 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
182 181 a1i ⊢ ( 𝑣 ∈ 𝐷 → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
183 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ∈ ( ∞Met ‘ ( 0 [,) +∞ ) ) )
184 182 7 183 sylancl ⊢ ( 𝑣 ∈ 𝐷 → ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ∈ ( ∞Met ‘ ( 0 [,) +∞ ) ) )
185 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ∈ ( ∞Met ‘ 𝐷 ) )
186 182 13 185 sylancl ⊢ ( 𝑣 ∈ 𝐷 → ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ∈ ( ∞Met ‘ 𝐷 ) )
187 117 a1i ⊢ ( 𝑣 ∈ 𝐷 → 0 ∈ ( 0 [,) +∞ ) )
188 id ⊢ ( 𝑣 ∈ 𝐷 → 𝑣 ∈ 𝐷 )
189 eqid ⊢ ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) = ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) )
190 2 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
191 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
192 189 190 191 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ) )
193 181 7 192 mp2an ⊢ ( 𝐽 ↾t ( 0 [,) +∞ ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
194 3 193 eqtri ⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) )
195 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) = ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) )
196 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) )
197 195 190 196 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐽 ↾t 𝐷 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ) )
198 181 13 197 mp2an ⊢ ( 𝐽 ↾t 𝐷 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) )
199 4 198 eqtri ⊢ 𝐿 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) )
200 194 199 190 txmetcnp ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) ∈ ( ∞Met ‘ ( 0 [,) +∞ ) ) ∧ ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) ∈ ( ∞Met ‘ 𝐷 ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) ∧ ( 0 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 0 , 𝑣 ⟩ ) ↔ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) ) ) )
201 184 186 182 187 188 200 syl32anc ⊢ ( 𝑣 ∈ 𝐷 → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 0 , 𝑣 ⟩ ) ↔ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( 0 ( ( abs ∘ − ) ↾ ( ( 0 [,) +∞ ) × ( 0 [,) +∞ ) ) ) 𝑎 ) < 𝑑 ∧ ( 𝑣 ( ( abs ∘ − ) ↾ ( 𝐷 × 𝐷 ) ) 𝑏 ) < 𝑑 ) → ( ( 0 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑣 ) ( abs ∘ − ) ( 𝑎 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) 𝑏 ) ) < 𝑒 ) ) ) )
202 112 180 201 mpbir2and ⊢ ( 𝑣 ∈ 𝐷 → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 0 , 𝑣 ⟩ ) )
203 202 ad2antlr ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 = 𝑢 ) → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 0 , 𝑣 ⟩ ) )
204 simpr ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 = 𝑢 ) → 0 = 𝑢 )
205 204 opeq1d ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 = 𝑢 ) → ⟨ 0 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
206 205 fveq2d ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 = 𝑢 ) → ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 0 , 𝑣 ⟩ ) = ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
207 203 206 eleqtrd ⊢ ( ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) ∧ 0 = 𝑢 ) → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
208 40 simprbi ⊢ ( 𝑢 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑢 )
209 208 adantr ⊢ ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) → 0 ≤ 𝑢 )
210 0re ⊢ 0 ∈ ℝ
211 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝑢 ∈ ℝ ) → ( 0 ≤ 𝑢 ↔ ( 0 < 𝑢 ∨ 0 = 𝑢 ) ) )
212 210 42 211 sylancr ⊢ ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) → ( 0 ≤ 𝑢 ↔ ( 0 < 𝑢 ∨ 0 = 𝑢 ) ) )
213 209 212 mpbid ⊢ ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) → ( 0 < 𝑢 ∨ 0 = 𝑢 ) )
214 111 207 213 mpjaodan ⊢ ( ( 𝑢 ∈ ( 0 [,) +∞ ) ∧ 𝑣 ∈ 𝐷 ) → ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
215 214 rgen2 ⊢ ∀ 𝑢 ∈ ( 0 [,) +∞ ) ∀ 𝑣 ∈ 𝐷 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
216 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ 𝑧 ) = ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
217 216 eleq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ 𝑧 ) ↔ ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
218 217 ralxp ⊢ ( ∀ 𝑧 ∈ ( ( 0 [,) +∞ ) × 𝐷 ) ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ 𝑧 ) ↔ ∀ 𝑢 ∈ ( 0 [,) +∞ ) ∀ 𝑣 ∈ 𝐷 ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
219 215 218 mpbir ⊢ ∀ 𝑧 ∈ ( ( 0 [,) +∞ ) × 𝐷 ) ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ 𝑧 )
220 cncnp ⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( ( 0 [,) +∞ ) × 𝐷 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ↔ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ ∧ ∀ 𝑧 ∈ ( ( 0 [,) +∞ ) × 𝐷 ) ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ 𝑧 ) ) ) )
221 93 21 220 mp2an ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ↔ ( ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) : ( ( 0 [,) +∞ ) × 𝐷 ) ⟶ ℂ ∧ ∀ 𝑧 ∈ ( ( 0 [,) +∞ ) × 𝐷 ) ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐾 ×t 𝐿 ) CnP 𝐽 ) ‘ 𝑧 ) ) )
222 20 219 221 mpbir2an ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) , 𝑦 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 )