cnheiborlem

	Ref	Expression
Hypotheses	cnheibor.2	$⊢ J = TopOpen (ℂ_{fld})$
	cnheibor.3	$⊢ T = J ↾_{𝑡} X$
	cnheibor.4	$⊢ F = (x \in ℝ, y \in ℝ ⟼ x + i y)$
	cnheibor.5	$⊢ Y = F [[- R, R] \times [- R, R]]$
Assertion	cnheiborlem	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to T \in Comp$

Proof

Step	Hyp	Ref	Expression
1		cnheibor.2	$⊢ J = TopOpen (ℂ_{fld})$
2		cnheibor.3	$⊢ T = J ↾_{𝑡} X$
3		cnheibor.4	$⊢ F = (x \in ℝ, y \in ℝ ⟼ x + i y)$
4		cnheibor.5	$⊢ Y = F [[- R, R] \times [- R, R]]$
5	1	cnfldtop	$⊢ J \in Top$
6	3	cnref1o	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} ℂ$
7		f1ofn	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to F Fn ℝ^{2}$
8		elpreima	$⊢ F Fn ℝ^{2} \to (u \in F^{-1} [X] \leftrightarrow (u \in ℝ^{2} \land F (u) \in X))$
9	6 7 8	mp2b	$⊢ u \in F^{-1} [X] \leftrightarrow (u \in ℝ^{2} \land F (u) \in X)$
10		1st2nd2	$⊢ u \in ℝ^{2} \to u = ⟨1^{st} (u), 2^{nd} (u)⟩$
11	10	ad2antrl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to u = ⟨1^{st} (u), 2^{nd} (u)⟩$
12		xp1st	$⊢ u \in ℝ^{2} \to 1^{st} (u) \in ℝ$
13	12	ad2antrl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 1^{st} (u) \in ℝ$
14	13	recnd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 1^{st} (u) \in ℂ$
15	14	abscld	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|1^{st} (u)\| \in ℝ$
16	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
17	16	toponunii	$⊢ ℂ = ⋃ J$
18	17	cldss	$⊢ X \in Clsd (J) \to X \subseteq ℂ$
19	18	adantr	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to X \subseteq ℂ$
20	19	adantr	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to X \subseteq ℂ$
21		simprr	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to F (u) \in X$
22	20 21	sseldd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to F (u) \in ℂ$
23	22	abscld	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|F (u)\| \in ℝ$
24		simplrl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to R \in ℝ$
25		simprl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to u \in ℝ^{2}$
26		f1ocnvfv1	$⊢ (F : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \land u \in ℝ^{2}) \to F^{-1} (F (u)) = u$
27	6 25 26	sylancr	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to F^{-1} (F (u)) = u$
28		fveq2	$⊢ z = F (u) \to ℜ (z) = ℜ (F (u))$
29		fveq2	$⊢ z = F (u) \to ℑ (z) = ℑ (F (u))$
30	28 29	opeq12d	$⊢ z = F (u) \to ⟨ℜ (z), ℑ (z)⟩ = ⟨ℜ (F (u)), ℑ (F (u))⟩$
31	3	cnrecnv	$⊢ F^{-1} = (z \in ℂ ⟼ ⟨ℜ (z), ℑ (z)⟩)$
32		opex	$⊢ ⟨ℜ (F (u)), ℑ (F (u))⟩ \in V$
33	30 31 32	fvmpt	$⊢ F (u) \in ℂ \to F^{-1} (F (u)) = ⟨ℜ (F (u)), ℑ (F (u))⟩$
34	22 33	syl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to F^{-1} (F (u)) = ⟨ℜ (F (u)), ℑ (F (u))⟩$
35	27 34	eqtr3d	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to u = ⟨ℜ (F (u)), ℑ (F (u))⟩$
36	35	fveq2d	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 1^{st} (u) = 1^{st} (⟨ℜ (F (u)), ℑ (F (u))⟩)$
37		fvex	$⊢ ℜ (F (u)) \in V$
38		fvex	$⊢ ℑ (F (u)) \in V$
39	37 38	op1st	$⊢ 1^{st} (⟨ℜ (F (u)), ℑ (F (u))⟩) = ℜ (F (u))$
40	36 39	eqtrdi	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 1^{st} (u) = ℜ (F (u))$
41	40	fveq2d	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|1^{st} (u)\| = \|ℜ (F (u))\|$
42		absrele	$⊢ F (u) \in ℂ \to \|ℜ (F (u))\| \leq \|F (u)\|$
43	22 42	syl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|ℜ (F (u))\| \leq \|F (u)\|$
44	41 43	eqbrtrd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|1^{st} (u)\| \leq \|F (u)\|$
45		fveq2	$⊢ z = F (u) \to \|z\| = \|F (u)\|$
46	45	breq1d	$⊢ z = F (u) \to (\|z\| \leq R \leftrightarrow \|F (u)\| \leq R)$
47		simplrr	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \forall z \in X \|z\| \leq R$
48	46 47 21	rspcdva	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|F (u)\| \leq R$
49	15 23 24 44 48	letrd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|1^{st} (u)\| \leq R$
50	13 24	absled	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to (\|1^{st} (u)\| \leq R \leftrightarrow (- R \leq 1^{st} (u) \land 1^{st} (u) \leq R))$
51	49 50	mpbid	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to (- R \leq 1^{st} (u) \land 1^{st} (u) \leq R)$
52	51	simpld	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to - R \leq 1^{st} (u)$
53	51	simprd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 1^{st} (u) \leq R$
54		renegcl	$⊢ R \in ℝ \to - R \in ℝ$
55	24 54	syl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to - R \in ℝ$
56		elicc2	$⊢ (- R \in ℝ \land R \in ℝ) \to (1^{st} (u) \in [- R, R] \leftrightarrow (1^{st} (u) \in ℝ \land - R \leq 1^{st} (u) \land 1^{st} (u) \leq R))$
57	55 24 56	syl2anc	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to (1^{st} (u) \in [- R, R] \leftrightarrow (1^{st} (u) \in ℝ \land - R \leq 1^{st} (u) \land 1^{st} (u) \leq R))$
58	13 52 53 57	mpbir3and	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 1^{st} (u) \in [- R, R]$
59		xp2nd	$⊢ u \in ℝ^{2} \to 2^{nd} (u) \in ℝ$
60	59	ad2antrl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 2^{nd} (u) \in ℝ$
61	60	recnd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 2^{nd} (u) \in ℂ$
62	61	abscld	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|2^{nd} (u)\| \in ℝ$
63	35	fveq2d	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 2^{nd} (u) = 2^{nd} (⟨ℜ (F (u)), ℑ (F (u))⟩)$
64	37 38	op2nd	$⊢ 2^{nd} (⟨ℜ (F (u)), ℑ (F (u))⟩) = ℑ (F (u))$
65	63 64	eqtrdi	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 2^{nd} (u) = ℑ (F (u))$
66	65	fveq2d	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|2^{nd} (u)\| = \|ℑ (F (u))\|$
67		absimle	$⊢ F (u) \in ℂ \to \|ℑ (F (u))\| \leq \|F (u)\|$
68	22 67	syl	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|ℑ (F (u))\| \leq \|F (u)\|$
69	66 68	eqbrtrd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|2^{nd} (u)\| \leq \|F (u)\|$
70	62 23 24 69 48	letrd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to \|2^{nd} (u)\| \leq R$
71	60 24	absled	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to (\|2^{nd} (u)\| \leq R \leftrightarrow (- R \leq 2^{nd} (u) \land 2^{nd} (u) \leq R))$
72	70 71	mpbid	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to (- R \leq 2^{nd} (u) \land 2^{nd} (u) \leq R)$
73	72	simpld	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to - R \leq 2^{nd} (u)$
74	72	simprd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 2^{nd} (u) \leq R$
75		elicc2	$⊢ (- R \in ℝ \land R \in ℝ) \to (2^{nd} (u) \in [- R, R] \leftrightarrow (2^{nd} (u) \in ℝ \land - R \leq 2^{nd} (u) \land 2^{nd} (u) \leq R))$
76	55 24 75	syl2anc	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to (2^{nd} (u) \in [- R, R] \leftrightarrow (2^{nd} (u) \in ℝ \land - R \leq 2^{nd} (u) \land 2^{nd} (u) \leq R))$
77	60 73 74 76	mpbir3and	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to 2^{nd} (u) \in [- R, R]$
78	58 77	opelxpd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to ⟨1^{st} (u), 2^{nd} (u)⟩ \in ([- R, R] \times [- R, R])$
79	11 78	eqeltrd	$⊢ ((X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \land (u \in ℝ^{2} \land F (u) \in X)) \to u \in ([- R, R] \times [- R, R])$
80	79	ex	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to ((u \in ℝ^{2} \land F (u) \in X) \to u \in ([- R, R] \times [- R, R]))$
81	9 80	syl5bi	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to (u \in F^{-1} [X] \to u \in ([- R, R] \times [- R, R]))$
82	81	ssrdv	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to F^{-1} [X] \subseteq [- R, R] \times [- R, R]$
83		f1ofun	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to Fun F$
84	6 83	ax-mp	$⊢ Fun F$
85		f1ofo	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to F : ℝ^{2} \underset{onto}{⟶} ℂ$
86		forn	$⊢ F : ℝ^{2} \underset{onto}{⟶} ℂ \to ran F = ℂ$
87	6 85 86	mp2b	$⊢ ran F = ℂ$
88	19 87	sseqtrrdi	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to X \subseteq ran F$
89		funimass1	$⊢ (Fun F \land X \subseteq ran F) \to (F^{-1} [X] \subseteq [- R, R] \times [- R, R] \to X \subseteq F [[- R, R] \times [- R, R]])$
90	84 88 89	sylancr	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to (F^{-1} [X] \subseteq [- R, R] \times [- R, R] \to X \subseteq F [[- R, R] \times [- R, R]])$
91	82 90	mpd	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to X \subseteq F [[- R, R] \times [- R, R]]$
92	91 4	sseqtrrdi	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to X \subseteq Y$
93		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
94	3 93 1	cnrehmeo	$⊢ F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Homeo J)$
95		imaexg	$⊢ F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Homeo J) \to F [[- R, R] \times [- R, R]] \in V$
96	94 95	ax-mp	$⊢ F [[- R, R] \times [- R, R]] \in V$
97	4 96	eqeltri	$⊢ Y \in V$
98	97	a1i	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to Y \in V$
99		restabs	$⊢ (J \in Top \land X \subseteq Y \land Y \in V) \to (J ↾_{𝑡} Y) ↾_{𝑡} X = J ↾_{𝑡} X$
100	5 92 98 99	mp3an2i	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to (J ↾_{𝑡} Y) ↾_{𝑡} X = J ↾_{𝑡} X$
101	100 2	eqtr4di	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to (J ↾_{𝑡} Y) ↾_{𝑡} X = T$
102	4	oveq2i	$⊢ J ↾_{𝑡} Y = J ↾_{𝑡} F [[- R, R] \times [- R, R]]$
103		ishmeo	$⊢ F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Homeo J) \leftrightarrow (F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Cn J) \land F^{-1} \in (J Cn (topGen (ran (.)) \times_{t} topGen (ran (.)))))$
104	94 103	mpbi	$⊢ (F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Cn J) \land F^{-1} \in (J Cn (topGen (ran (.)) \times_{t} topGen (ran (.)))))$
105	104	simpli	$⊢ F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Cn J)$
106		iccssre	$⊢ (- R \in ℝ \land R \in ℝ) \to [- R, R] \subseteq ℝ$
107	54 106	mpancom	$⊢ R \in ℝ \to [- R, R] \subseteq ℝ$
108	1 93	rerest	$⊢ [- R, R] \subseteq ℝ \to J ↾_{𝑡} [- R, R] = topGen (ran (.)) ↾_{𝑡} [- R, R]$
109	107 108	syl	$⊢ R \in ℝ \to J ↾_{𝑡} [- R, R] = topGen (ran (.)) ↾_{𝑡} [- R, R]$
110	109 109	oveq12d	$⊢ R \in ℝ \to (J ↾_{𝑡} [- R, R]) \times_{t} (J ↾_{𝑡} [- R, R]) = (topGen (ran (.)) ↾_{𝑡} [- R, R]) \times_{t} (topGen (ran (.)) ↾_{𝑡} [- R, R])$
111		retop	$⊢ topGen (ran (.)) \in Top$
112		ovex	$⊢ [- R, R] \in V$
113		txrest	$⊢ ((topGen (ran (.)) \in Top \land topGen (ran (.)) \in Top) \land ([- R, R] \in V \land [- R, R] \in V)) \to (topGen (ran (.)) \times_{t} topGen (ran (.))) ↾_{𝑡} ([- R, R] \times [- R, R]) = (topGen (ran (.)) ↾_{𝑡} [- R, R]) \times_{t} (topGen (ran (.)) ↾_{𝑡} [- R, R])$
114	111 111 112 112 113	mp4an	$⊢ (topGen (ran (.)) \times_{t} topGen (ran (.))) ↾_{𝑡} ([- R, R] \times [- R, R]) = (topGen (ran (.)) ↾_{𝑡} [- R, R]) \times_{t} (topGen (ran (.)) ↾_{𝑡} [- R, R])$
115	110 114	eqtr4di	$⊢ R \in ℝ \to (J ↾_{𝑡} [- R, R]) \times_{t} (J ↾_{𝑡} [- R, R]) = (topGen (ran (.)) \times_{t} topGen (ran (.))) ↾_{𝑡} ([- R, R] \times [- R, R])$
116		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [- R, R] = topGen (ran (.)) ↾_{𝑡} [- R, R]$
117	93 116	icccmp	$⊢ (- R \in ℝ \land R \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [- R, R] \in Comp$
118	54 117	mpancom	$⊢ R \in ℝ \to topGen (ran (.)) ↾_{𝑡} [- R, R] \in Comp$
119	109 118	eqeltrd	$⊢ R \in ℝ \to J ↾_{𝑡} [- R, R] \in Comp$
120		txcmp	$⊢ (J ↾_{𝑡} [- R, R] \in Comp \land J ↾_{𝑡} [- R, R] \in Comp) \to (J ↾_{𝑡} [- R, R]) \times_{t} (J ↾_{𝑡} [- R, R]) \in Comp$
121	119 119 120	syl2anc	$⊢ R \in ℝ \to (J ↾_{𝑡} [- R, R]) \times_{t} (J ↾_{𝑡} [- R, R]) \in Comp$
122	115 121	eqeltrrd	$⊢ R \in ℝ \to (topGen (ran (.)) \times_{t} topGen (ran (.))) ↾_{𝑡} ([- R, R] \times [- R, R]) \in Comp$
123		imacmp	$⊢ (F \in ((topGen (ran (.)) \times_{t} topGen (ran (.))) Cn J) \land (topGen (ran (.)) \times_{t} topGen (ran (.))) ↾_{𝑡} ([- R, R] \times [- R, R]) \in Comp) \to J ↾_{𝑡} F [[- R, R] \times [- R, R]] \in Comp$
124	105 122 123	sylancr	$⊢ R \in ℝ \to J ↾_{𝑡} F [[- R, R] \times [- R, R]] \in Comp$
125	102 124	eqeltrid	$⊢ R \in ℝ \to J ↾_{𝑡} Y \in Comp$
126	125	ad2antrl	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to J ↾_{𝑡} Y \in Comp$
127		imassrn	$⊢ F [[- R, R] \times [- R, R]] \subseteq ran F$
128	4 127	eqsstri	$⊢ Y \subseteq ran F$
129		f1of	$⊢ F : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to F : ℝ^{2} ⟶ ℂ$
130		frn	$⊢ F : ℝ^{2} ⟶ ℂ \to ran F \subseteq ℂ$
131	6 129 130	mp2b	$⊢ ran F \subseteq ℂ$
132	128 131	sstri	$⊢ Y \subseteq ℂ$
133		simpl	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to X \in Clsd (J)$
134	17	restcldi	$⊢ (Y \subseteq ℂ \land X \in Clsd (J) \land X \subseteq Y) \to X \in Clsd (J ↾_{𝑡} Y)$
135	132 133 92 134	mp3an2i	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to X \in Clsd (J ↾_{𝑡} Y)$
136		cmpcld	$⊢ (J ↾_{𝑡} Y \in Comp \land X \in Clsd (J ↾_{𝑡} Y)) \to (J ↾_{𝑡} Y) ↾_{𝑡} X \in Comp$
137	126 135 136	syl2anc	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to (J ↾_{𝑡} Y) ↾_{𝑡} X \in Comp$
138	101 137	eqeltrrd	$⊢ (X \in Clsd (J) \land (R \in ℝ \land \forall z \in X \|z\| \leq R)) \to T \in Comp$

Metamath Proof Explorer

Theorem cnheiborlem

Proof