xrlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +oo . Since any ~>r limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015)

	Ref	Expression
Hypotheses	xrlimcnp.a	$⊢ φ \to A = B \cup \{+∞\}$
	xrlimcnp.b	$⊢ φ \to B \subseteq ℝ$
	xrlimcnp.r	$⊢ (φ \land x \in A) \to R \in ℂ$
	xrlimcnp.c	$⊢ x = +∞ \to R = C$
	xrlimcnp.j	$⊢ J = TopOpen (ℂ_{fld})$
	xrlimcnp.k	$⊢ K = ordTop (\leq) ↾_{𝑡} A$
Assertion	xrlimcnp	$⊢ φ \to ((x \in B ⟼ R) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ R) \in (K CnP J) (+∞))$

Proof

Step	Hyp	Ref	Expression
1		xrlimcnp.a	$⊢ φ \to A = B \cup \{+∞\}$
2		xrlimcnp.b	$⊢ φ \to B \subseteq ℝ$
3		xrlimcnp.r	$⊢ (φ \land x \in A) \to R \in ℂ$
4		xrlimcnp.c	$⊢ x = +∞ \to R = C$
5		xrlimcnp.j	$⊢ J = TopOpen (ℂ_{fld})$
6		xrlimcnp.k	$⊢ K = ordTop (\leq) ↾_{𝑡} A$
7	3	fmpttd	$⊢ φ \to (x \in A ⟼ R) : A ⟶ ℂ$
8	7	adantr	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to (x \in A ⟼ R) : A ⟶ ℂ$
9		eqid	$⊢ (x \in A ⟼ R) = (x \in A ⟼ R)$
10		ssun2	$⊢ \{+∞\} \subseteq B \cup \{+∞\}$
11		pnfex	$⊢ +∞ \in V$
12	11	snid	$⊢ +∞ \in \{+∞\}$
13	10 12	sselii	$⊢ +∞ \in (B \cup \{+∞\})$
14	13 1	eleqtrrid	$⊢ φ \to +∞ \in A$
15	4	eleq1d	$⊢ x = +∞ \to (R \in ℂ \leftrightarrow C \in ℂ)$
16	3	ralrimiva	$⊢ φ \to \forall x \in A R \in ℂ$
17	15 16 14	rspcdva	$⊢ φ \to C \in ℂ$
18	9 4 14 17	fvmptd3	$⊢ φ \to (x \in A ⟼ R) (+∞) = C$
19	18	ad2antrr	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land y \in J) \to (x \in A ⟼ R) (+∞) = C$
20	19	eleq1d	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land y \in J) \to ((x \in A ⟼ R) (+∞) \in y \leftrightarrow C \in y)$
21		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
22	5	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
23	22	mopni2	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in J \land C \in y) \to \exists r \in ℝ^{+} C ball (abs \circ -) r \subseteq y$
24	21 23	mp3an1	$⊢ (y \in J \land C \in y) \to \exists r \in ℝ^{+} C ball (abs \circ -) r \subseteq y$
25		ssun1	$⊢ B \subseteq B \cup \{+∞\}$
26	25 1	sseqtrrid	$⊢ φ \to B \subseteq A$
27		ssralv	$⊢ B \subseteq A \to (\forall x \in A R \in ℂ \to \forall x \in B R \in ℂ)$
28	26 16 27	sylc	$⊢ φ \to \forall x \in B R \in ℂ$
29	28	ad2antrr	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to \forall x \in B R \in ℂ$
30		simprl	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to r \in ℝ^{+}$
31		simplr	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to (x \in B ⟼ R) \underset{ℝ}{⇝} C$
32	29 30 31	rlimi	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to \exists k \in ℝ \forall x \in B (k \leq x \to \|R - C\| < r)$
33		letop	$⊢ ordTop (\leq) \in Top$
34		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
35	2 34	sstrdi	$⊢ φ \to B \subseteq ℝ^{*}$
36		pnfxr	$⊢ +∞ \in ℝ^{*}$
37	36	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
38	37	snssd	$⊢ φ \to \{+∞\} \subseteq ℝ^{*}$
39	35 38	unssd	$⊢ φ \to B \cup \{+∞\} \subseteq ℝ^{*}$
40	1 39	eqsstrd	$⊢ φ \to A \subseteq ℝ^{*}$
41		xrex	$⊢ ℝ^{*} \in V$
42	41	ssex	$⊢ A \subseteq ℝ^{*} \to A \in V$
43	40 42	syl	$⊢ φ \to A \in V$
44	43	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to A \in V$
45		iocpnfordt	$⊢ (k, +∞] \in ordTop (\leq)$
46	45	a1i	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (k, +∞] \in ordTop (\leq)$
47		elrestr	$⊢ (ordTop (\leq) \in Top \land A \in V \land (k, +∞] \in ordTop (\leq)) \to (k, +∞] \cap A \in (ordTop (\leq) ↾_{𝑡} A)$
48	33 44 46 47	mp3an2i	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (k, +∞] \cap A \in (ordTop (\leq) ↾_{𝑡} A)$
49	48 6	eleqtrrdi	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (k, +∞] \cap A \in K$
50		simprl	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to k \in ℝ$
51	50	rexrd	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to k \in ℝ^{*}$
52	36	a1i	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to +∞ \in ℝ^{*}$
53	50	ltpnfd	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to k < +∞$
54		ubioc1	$⊢ (k \in ℝ^{} \land +∞ \in ℝ^{} \land k < +∞) \to +∞ \in (k, +∞]$
55	51 52 53 54	syl3anc	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to +∞ \in (k, +∞]$
56	14	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to +∞ \in A$
57	55 56	elind	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to +∞ \in ((k, +∞] \cap A)$
58		simplr	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to k \in ℝ$
59	58	rexrd	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to k \in ℝ^{*}$
60		elioc1	$⊢ (k \in ℝ^{} \land +∞ \in ℝ^{}) \to (x \in (k, +∞] \leftrightarrow (x \in ℝ^{*} \land k < x \land x \leq +∞))$
61	59 36 60	sylancl	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (x \in (k, +∞] \leftrightarrow (x \in ℝ^{*} \land k < x \land x \leq +∞))$
62		simp2	$⊢ (x \in ℝ^{*} \land k < x \land x \leq +∞) \to k < x$
63	61 62	biimtrdi	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (x \in (k, +∞] \to k < x)$
64	2	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \to B \subseteq ℝ$
65	64	sselda	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to x \in ℝ$
66		ltle	$⊢ (k \in ℝ \land x \in ℝ) \to (k < x \to k \leq x)$
67	58 65 66	syl2anc	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (k < x \to k \leq x)$
68	63 67	syld	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (x \in (k, +∞] \to k \leq x)$
69	21	a1i	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to abs \circ - \in ∞Met (ℂ)$
70		simprl	$⊢ (φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to r \in ℝ^{+}$
71	70	ad2antrr	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to r \in ℝ^{+}$
72		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
73	71 72	syl	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to r \in ℝ^{*}$
74	17	ad3antrrr	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to C \in ℂ$
75	28	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \to \forall x \in B R \in ℂ$
76	75	r19.21bi	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to R \in ℂ$
77		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land r \in ℝ^{*}) \land (C \in ℂ \land R \in ℂ)) \to (R \in (C ball (abs \circ -) r) \leftrightarrow R (abs \circ -) C < r)$
78	69 73 74 76 77	syl22anc	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (R \in (C ball (abs \circ -) r) \leftrightarrow R (abs \circ -) C < r)$
79		eqid	$⊢ abs \circ - = abs \circ -$
80	79	cnmetdval	$⊢ (R \in ℂ \land C \in ℂ) \to R (abs \circ -) C = \|R - C\|$
81	76 74 80	syl2anc	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to R (abs \circ -) C = \|R - C\|$
82	81	breq1d	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (R (abs \circ -) C < r \leftrightarrow \|R - C\| < r)$
83	78 82	bitrd	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (R \in (C ball (abs \circ -) r) \leftrightarrow \|R - C\| < r)$
84	83	biimprd	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to (\|R - C\| < r \to R \in (C ball (abs \circ -) r))$
85	68 84	imim12d	$⊢ (((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \land x \in B) \to ((k \leq x \to \|R - C\| < r) \to (x \in (k, +∞] \to R \in (C ball (abs \circ -) r)))$
86	85	ralimdva	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land k \in ℝ) \to (\forall x \in B (k \leq x \to \|R - C\| < r) \to \forall x \in B (x \in (k, +∞] \to R \in (C ball (abs \circ -) r)))$
87	86	impr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to \forall x \in B (x \in (k, +∞] \to R \in (C ball (abs \circ -) r))$
88	17	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to C \in ℂ$
89		simplrl	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to r \in ℝ^{+}$
90		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land C \in ℂ \land r \in ℝ^{+}) \to C \in (C ball (abs \circ -) r)$
91	21 88 89 90	mp3an2i	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to C \in (C ball (abs \circ -) r)$
92	91	a1d	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (+∞ \in (k, +∞] \to C \in (C ball (abs \circ -) r))$
93		eleq1	$⊢ x = +∞ \to (x \in (k, +∞] \leftrightarrow +∞ \in (k, +∞])$
94	4	eleq1d	$⊢ x = +∞ \to (R \in (C ball (abs \circ -) r) \leftrightarrow C \in (C ball (abs \circ -) r))$
95	93 94	imbi12d	$⊢ x = +∞ \to ((x \in (k, +∞] \to R \in (C ball (abs \circ -) r)) \leftrightarrow (+∞ \in (k, +∞] \to C \in (C ball (abs \circ -) r)))$
96	11 95	ralsn	$⊢ \forall x \in \{+∞\} (x \in (k, +∞] \to R \in (C ball (abs \circ -) r)) \leftrightarrow (+∞ \in (k, +∞] \to C \in (C ball (abs \circ -) r))$
97	92 96	sylibr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to \forall x \in \{+∞\} (x \in (k, +∞] \to R \in (C ball (abs \circ -) r))$
98		ralunb	$⊢ \forall x \in (B \cup \{+∞\}) (x \in (k, +∞] \to R \in (C ball (abs \circ -) r)) \leftrightarrow (\forall x \in B (x \in (k, +∞] \to R \in (C ball (abs \circ -) r)) \land \forall x \in \{+∞\} (x \in (k, +∞] \to R \in (C ball (abs \circ -) r)))$
99	87 97 98	sylanbrc	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to \forall x \in (B \cup \{+∞\}) (x \in (k, +∞] \to R \in (C ball (abs \circ -) r))$
100	1	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to A = B \cup \{+∞\}$
101	99 100	raleqtrrdv	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to \forall x \in A (x \in (k, +∞] \to R \in (C ball (abs \circ -) r))$
102	101	ss2rabd	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to \{x \in A \| x \in (k, +∞]\} \subseteq \{x \in A \| R \in (C ball (abs \circ -) r)\}$
103		dfin5	$⊢ A \cap (k, +∞] = \{x \in A \| x \in (k, +∞]\}$
104	103	ineqcomi	$⊢ (k, +∞] \cap A = \{x \in A \| x \in (k, +∞]\}$
105	9	mptpreima	$⊢ {(x \in A ⟼ R)}^{-1} [C ball (abs \circ -) r] = \{x \in A \| R \in (C ball (abs \circ -) r)\}$
106	102 104 105	3sstr4g	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (k, +∞] \cap A \subseteq {(x \in A ⟼ R)}^{-1} [C ball (abs \circ -) r]$
107		funmpt	$⊢ Fun (x \in A ⟼ R)$
108		inss2	$⊢ (k, +∞] \cap A \subseteq A$
109	7	ad2antrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (x \in A ⟼ R) : A ⟶ ℂ$
110	109	fdmd	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to dom (x \in A ⟼ R) = A$
111	108 110	sseqtrrid	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (k, +∞] \cap A \subseteq dom (x \in A ⟼ R)$
112		funimass3	$⊢ (Fun (x \in A ⟼ R) \land (k, +∞] \cap A \subseteq dom (x \in A ⟼ R)) \to ((x \in A ⟼ R) [(k, +∞] \cap A] \subseteq C ball (abs \circ -) r \leftrightarrow (k, +∞] \cap A \subseteq {(x \in A ⟼ R)}^{-1} [C ball (abs \circ -) r])$
113	107 111 112	sylancr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to ((x \in A ⟼ R) [(k, +∞] \cap A] \subseteq C ball (abs \circ -) r \leftrightarrow (k, +∞] \cap A \subseteq {(x \in A ⟼ R)}^{-1} [C ball (abs \circ -) r])$
114	106 113	mpbird	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (x \in A ⟼ R) [(k, +∞] \cap A] \subseteq C ball (abs \circ -) r$
115		simplrr	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to C ball (abs \circ -) r \subseteq y$
116	114 115	sstrd	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to (x \in A ⟼ R) [(k, +∞] \cap A] \subseteq y$
117		eleq2	$⊢ z = (k, +∞] \cap A \to (+∞ \in z \leftrightarrow +∞ \in ((k, +∞] \cap A))$
118		imaeq2	$⊢ z = (k, +∞] \cap A \to (x \in A ⟼ R) [z] = (x \in A ⟼ R) [(k, +∞] \cap A]$
119	118	sseq1d	$⊢ z = (k, +∞] \cap A \to ((x \in A ⟼ R) [z] \subseteq y \leftrightarrow (x \in A ⟼ R) [(k, +∞] \cap A] \subseteq y)$
120	117 119	anbi12d	$⊢ z = (k, +∞] \cap A \to ((+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y) \leftrightarrow (+∞ \in ((k, +∞] \cap A) \land (x \in A ⟼ R) [(k, +∞] \cap A] \subseteq y))$
121	120	rspcev	$⊢ ((k, +∞] \cap A \in K \land (+∞ \in ((k, +∞] \cap A) \land (x \in A ⟼ R) [(k, +∞] \cap A] \subseteq y)) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y)$
122	49 57 116 121	syl12anc	$⊢ ((φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \land (k \in ℝ \land \forall x \in B (k \leq x \to \|R - C\| < r))) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y)$
123	122	rexlimdvaa	$⊢ (φ \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to (\exists k \in ℝ \forall x \in B (k \leq x \to \|R - C\| < r) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
124	123	adantlr	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to (\exists k \in ℝ \forall x \in B (k \leq x \to \|R - C\| < r) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
125	32 124	mpd	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land (r \in ℝ^{+} \land C ball (abs \circ -) r \subseteq y)) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y)$
126	125	rexlimdvaa	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to (\exists r \in ℝ^{+} C ball (abs \circ -) r \subseteq y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
127	24 126	syl5	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to ((y \in J \land C \in y) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
128	127	expdimp	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land y \in J) \to (C \in y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
129	20 128	sylbid	$⊢ ((φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \land y \in J) \to ((x \in A ⟼ R) (+∞) \in y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
130	129	ralrimiva	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to \forall y \in J ((x \in A ⟼ R) (+∞) \in y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))$
131		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
132		resttopon	$⊢ (ordTop (\leq) \in TopOn (ℝ^{}) \land A \subseteq ℝ^{}) \to ordTop (\leq) ↾_{𝑡} A \in TopOn (A)$
133	131 40 132	sylancr	$⊢ φ \to ordTop (\leq) ↾_{𝑡} A \in TopOn (A)$
134	6 133	eqeltrid	$⊢ φ \to K \in TopOn (A)$
135	5	cnfldtopon	$⊢ J \in TopOn (ℂ)$
136	135	a1i	$⊢ φ \to J \in TopOn (ℂ)$
137		iscnp	$⊢ (K \in TopOn (A) \land J \in TopOn (ℂ) \land +∞ \in A) \to ((x \in A ⟼ R) \in (K CnP J) (+∞) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall y \in J ((x \in A ⟼ R) (+∞) \in y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))))$
138	134 136 14 137	syl3anc	$⊢ φ \to ((x \in A ⟼ R) \in (K CnP J) (+∞) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall y \in J ((x \in A ⟼ R) (+∞) \in y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))))$
139	138	adantr	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to ((x \in A ⟼ R) \in (K CnP J) (+∞) \leftrightarrow ((x \in A ⟼ R) : A ⟶ ℂ \land \forall y \in J ((x \in A ⟼ R) (+∞) \in y \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq y))))$
140	8 130 139	mpbir2and	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to (x \in A ⟼ R) \in (K CnP J) (+∞)$
141		simplr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (x \in A ⟼ R) \in (K CnP J) (+∞)$
142	17	ad2antrr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to C \in ℂ$
143	72	adantl	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to r \in ℝ^{*}$
144	22	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land C \in ℂ \land r \in ℝ^{*}) \to C ball (abs \circ -) r \in J$
145	21 142 143 144	mp3an2i	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to C ball (abs \circ -) r \in J$
146	18	ad2antrr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (x \in A ⟼ R) (+∞) = C$
147		simpr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
148	21 142 147 90	mp3an2i	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to C \in (C ball (abs \circ -) r)$
149	146 148	eqeltrd	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (x \in A ⟼ R) (+∞) \in (C ball (abs \circ -) r)$
150		cnpimaex	$⊢ ((x \in A ⟼ R) \in (K CnP J) (+∞) \land C ball (abs \circ -) r \in J \land (x \in A ⟼ R) (+∞) \in (C ball (abs \circ -) r)) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq C ball (abs \circ -) r)$
151	141 145 149 150	syl3anc	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to \exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq C ball (abs \circ -) r)$
152		vex	$⊢ w \in V$
153	152	inex1	$⊢ w \cap A \in V$
154	153	a1i	$⊢ (((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \land w \in ordTop (\leq)) \to w \cap A \in V$
155	6	eleq2i	$⊢ z \in K \leftrightarrow z \in (ordTop (\leq) ↾_{𝑡} A)$
156	43	ad2antrr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to A \in V$
157		elrest	$⊢ (ordTop (\leq) \in Top \land A \in V) \to (z \in (ordTop (\leq) ↾_{𝑡} A) \leftrightarrow \exists w \in ordTop (\leq) z = w \cap A)$
158	33 156 157	sylancr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (z \in (ordTop (\leq) ↾_{𝑡} A) \leftrightarrow \exists w \in ordTop (\leq) z = w \cap A)$
159	155 158	bitrid	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (z \in K \leftrightarrow \exists w \in ordTop (\leq) z = w \cap A)$
160		eleq2	$⊢ z = w \cap A \to (+∞ \in z \leftrightarrow +∞ \in (w \cap A))$
161		imaeq2	$⊢ z = w \cap A \to (x \in A ⟼ R) [z] = (x \in A ⟼ R) [w \cap A]$
162	161	sseq1d	$⊢ z = w \cap A \to ((x \in A ⟼ R) [z] \subseteq C ball (abs \circ -) r \leftrightarrow (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r)$
163	160 162	anbi12d	$⊢ z = w \cap A \to ((+∞ \in z \land (x \in A ⟼ R) [z] \subseteq C ball (abs \circ -) r) \leftrightarrow (+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r))$
164	163	adantl	$⊢ (((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \land z = w \cap A) \to ((+∞ \in z \land (x \in A ⟼ R) [z] \subseteq C ball (abs \circ -) r) \leftrightarrow (+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r))$
165	154 159 164	rexxfr2d	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (\exists z \in K (+∞ \in z \land (x \in A ⟼ R) [z] \subseteq C ball (abs \circ -) r) \leftrightarrow \exists w \in ordTop (\leq) (+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r))$
166	151 165	mpbid	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to \exists w \in ordTop (\leq) (+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r)$
167		elinel1	$⊢ +∞ \in (w \cap A) \to +∞ \in w$
168		pnfnei	$⊢ (w \in ordTop (\leq) \land +∞ \in w) \to \exists k \in ℝ (k, +∞] \subseteq w$
169	167 168	sylan2	$⊢ (w \in ordTop (\leq) \land +∞ \in (w \cap A)) \to \exists k \in ℝ (k, +∞] \subseteq w$
170		df-ima	$⊢ (x \in A ⟼ R) [w \cap A] = ran ({(x \in A ⟼ R) ↾}_{(w \cap A)})$
171		inss2	$⊢ w \cap A \subseteq A$
172		resmpt	$⊢ w \cap A \subseteq A \to {(x \in A ⟼ R) ↾}_{(w \cap A)} = (x \in (w \cap A) ⟼ R)$
173	171 172	ax-mp	$⊢ {(x \in A ⟼ R) ↾}_{(w \cap A)} = (x \in (w \cap A) ⟼ R)$
174	173	rneqi	$⊢ ran ({(x \in A ⟼ R) ↾}_{(w \cap A)}) = ran (x \in (w \cap A) ⟼ R)$
175	170 174	eqtri	$⊢ (x \in A ⟼ R) [w \cap A] = ran (x \in (w \cap A) ⟼ R)$
176	175	sseq1i	$⊢ (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \leftrightarrow ran (x \in (w \cap A) ⟼ R) \subseteq C ball (abs \circ -) r$
177		dfss3	$⊢ ran (x \in (w \cap A) ⟼ R) \subseteq C ball (abs \circ -) r \leftrightarrow \forall z \in ran (x \in (w \cap A) ⟼ R) z \in (C ball (abs \circ -) r)$
178	176 177	bitri	$⊢ (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \leftrightarrow \forall z \in ran (x \in (w \cap A) ⟼ R) z \in (C ball (abs \circ -) r)$
179	16	adantr	$⊢ (φ \land r \in ℝ^{+}) \to \forall x \in A R \in ℂ$
180		ssralv	$⊢ w \cap A \subseteq A \to (\forall x \in A R \in ℂ \to \forall x \in (w \cap A) R \in ℂ)$
181	171 179 180	mpsyl	$⊢ (φ \land r \in ℝ^{+}) \to \forall x \in (w \cap A) R \in ℂ$
182		eqid	$⊢ (x \in (w \cap A) ⟼ R) = (x \in (w \cap A) ⟼ R)$
183		eleq1	$⊢ z = R \to (z \in (C ball (abs \circ -) r) \leftrightarrow R \in (C ball (abs \circ -) r))$
184	182 183	ralrnmptw	$⊢ \forall x \in (w \cap A) R \in ℂ \to (\forall z \in ran (x \in (w \cap A) ⟼ R) z \in (C ball (abs \circ -) r) \leftrightarrow \forall x \in (w \cap A) R \in (C ball (abs \circ -) r))$
185	181 184	syl	$⊢ (φ \land r \in ℝ^{+}) \to (\forall z \in ran (x \in (w \cap A) ⟼ R) z \in (C ball (abs \circ -) r) \leftrightarrow \forall x \in (w \cap A) R \in (C ball (abs \circ -) r))$
186	185	biimpd	$⊢ (φ \land r \in ℝ^{+}) \to (\forall z \in ran (x \in (w \cap A) ⟼ R) z \in (C ball (abs \circ -) r) \to \forall x \in (w \cap A) R \in (C ball (abs \circ -) r))$
187	178 186	biimtrid	$⊢ (φ \land r \in ℝ^{+}) \to ((x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \to \forall x \in (w \cap A) R \in (C ball (abs \circ -) r))$
188		simplrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to (k, +∞] \subseteq w$
189	35	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to B \subseteq ℝ^{*}$
190		simprl	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in B$
191	189 190	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in ℝ^{*}$
192		simprr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to k < x$
193	191	pnfged	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \leq +∞$
194		simplrl	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to k \in ℝ$
195	194	rexrd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to k \in ℝ^{*}$
196	195 36 60	sylancl	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to (x \in (k, +∞] \leftrightarrow (x \in ℝ^{*} \land k < x \land x \leq +∞))$
197	191 192 193 196	mpbir3and	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in (k, +∞]$
198	188 197	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in w$
199	26	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to B \subseteq A$
200	199	sselda	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land x \in B) \to x \in A$
201	200	adantrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in A$
202	198 201	elind	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in (w \cap A)$
203	202	ex	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to ((x \in B \land k < x) \to x \in (w \cap A))$
204	203	imim1d	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to ((x \in (w \cap A) \to R \in (C ball (abs \circ -) r)) \to ((x \in B \land k < x) \to R \in (C ball (abs \circ -) r)))$
205	21	a1i	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to abs \circ - \in ∞Met (ℂ)$
206	72	adantl	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℝ^{*}$
207	206	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to r \in ℝ^{*}$
208	17	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to C \in ℂ$
209	28	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to \forall x \in B R \in ℂ$
210	209	r19.21bi	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land x \in B) \to R \in ℂ$
211	210	adantrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to R \in ℂ$
212	205 207 208 211 77	syl22anc	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to (R \in (C ball (abs \circ -) r) \leftrightarrow R (abs \circ -) C < r)$
213	211 208 80	syl2anc	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to R (abs \circ -) C = \|R - C\|$
214	213	breq1d	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to (R (abs \circ -) C < r \leftrightarrow \|R - C\| < r)$
215	212 214	bitrd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to (R \in (C ball (abs \circ -) r) \leftrightarrow \|R - C\| < r)$
216	215	pm5.74da	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to (((x \in B \land k < x) \to R \in (C ball (abs \circ -) r)) \leftrightarrow ((x \in B \land k < x) \to \|R - C\| < r))$
217	204 216	sylibd	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to ((x \in (w \cap A) \to R \in (C ball (abs \circ -) r)) \to ((x \in B \land k < x) \to \|R - C\| < r))$
218	217	exp4a	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to ((x \in (w \cap A) \to R \in (C ball (abs \circ -) r)) \to (x \in B \to (k < x \to \|R - C\| < r)))$
219	218	ralimdv2	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to (\forall x \in (w \cap A) R \in (C ball (abs \circ -) r) \to \forall x \in B (k < x \to \|R - C\| < r))$
220	219	imp	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land \forall x \in (w \cap A) R \in (C ball (abs \circ -) r)) \to \forall x \in B (k < x \to \|R - C\| < r)$
221	220	an32s	$⊢ (((φ \land r \in ℝ^{+}) \land \forall x \in (w \cap A) R \in (C ball (abs \circ -) r)) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to \forall x \in B (k < x \to \|R - C\| < r)$
222	221	expr	$⊢ (((φ \land r \in ℝ^{+}) \land \forall x \in (w \cap A) R \in (C ball (abs \circ -) r)) \land k \in ℝ) \to ((k, +∞] \subseteq w \to \forall x \in B (k < x \to \|R - C\| < r))$
223	222	reximdva	$⊢ ((φ \land r \in ℝ^{+}) \land \forall x \in (w \cap A) R \in (C ball (abs \circ -) r)) \to (\exists k \in ℝ (k, +∞] \subseteq w \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
224	223	ex	$⊢ (φ \land r \in ℝ^{+}) \to (\forall x \in (w \cap A) R \in (C ball (abs \circ -) r) \to (\exists k \in ℝ (k, +∞] \subseteq w \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r)))$
225	187 224	syld	$⊢ (φ \land r \in ℝ^{+}) \to ((x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \to (\exists k \in ℝ (k, +∞] \subseteq w \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r)))$
226	225	com23	$⊢ (φ \land r \in ℝ^{+}) \to (\exists k \in ℝ (k, +∞] \subseteq w \to ((x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r)))$
227	169 226	syl5	$⊢ (φ \land r \in ℝ^{+}) \to ((w \in ordTop (\leq) \land +∞ \in (w \cap A)) \to ((x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r)))$
228	227	impl	$⊢ (((φ \land r \in ℝ^{+}) \land w \in ordTop (\leq)) \land +∞ \in (w \cap A)) \to ((x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
229	228	expimpd	$⊢ ((φ \land r \in ℝ^{+}) \land w \in ordTop (\leq)) \to ((+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r) \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
230	229	rexlimdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists w \in ordTop (\leq) (+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r) \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
231	230	adantlr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (\exists w \in ordTop (\leq) (+∞ \in (w \cap A) \land (x \in A ⟼ R) [w \cap A] \subseteq C ball (abs \circ -) r) \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
232	166 231	mpd	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r)$
233	232	ralrimiva	$⊢ (φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \to \forall r \in ℝ^{+} \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r)$
234	28 2 17	rlim2lt	$⊢ φ \to ((x \in B ⟼ R) \underset{ℝ}{⇝} C \leftrightarrow \forall r \in ℝ^{+} \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
235	234	adantr	$⊢ (φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \to ((x \in B ⟼ R) \underset{ℝ}{⇝} C \leftrightarrow \forall r \in ℝ^{+} \exists k \in ℝ \forall x \in B (k < x \to \|R - C\| < r))$
236	233 235	mpbird	$⊢ (φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \to (x \in B ⟼ R) \underset{ℝ}{⇝} C$
237	140 236	impbida	$⊢ φ \to ((x \in B ⟼ R) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ R) \in (K CnP J) (+∞))$

Metamath Proof Explorer

Theorem xrlimcnp

Proof