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		ss2rab	$⊢ \{x \in A \| x \in (k, +∞]\} \subseteq \{x \in A \| R \in (C ball (abs \circ -) r)\} \leftrightarrow \forall x \in A (x \in (k, +∞] \to R \in (C ball (abs \circ -) r))$
103	101 102	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 \{x \in A \| x \in (k, +∞]\} \subseteq \{x \in A \| R \in (C ball (abs \circ -) r)\}$
104		incom	$⊢ (k, +∞] \cap A = A \cap (k, +∞]$
105		dfin5	$⊢ A \cap (k, +∞] = \{x \in A \| x \in (k, +∞]\}$
106	104 105	eqtri	$⊢ (k, +∞] \cap A = \{x \in A \| x \in (k, +∞]\}$
107	9	mptpreima	$⊢ {(x \in A ⟼ R)}^{-1} [C ball (abs \circ -) r] = \{x \in A \| R \in (C ball (abs \circ -) r)\}$
108	103 106 107	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]$
109		funmpt	$⊢ Fun (x \in A ⟼ R)$
110		inss2	$⊢ (k, +∞] \cap A \subseteq A$
111	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 ⟶ ℂ$
112	111	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$
113	110 112	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)$
114		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])$
115	109 113 114	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])$
116	108 115	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$
117		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$
118	116 117	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$
119		eleq2	$⊢ z = (k, +∞] \cap A \to (+∞ \in z \leftrightarrow +∞ \in ((k, +∞] \cap A))$
120		imaeq2	$⊢ z = (k, +∞] \cap A \to (x \in A ⟼ R) [z] = (x \in A ⟼ R) [(k, +∞] \cap A]$
121	120	sseq1d	$⊢ z = (k, +∞] \cap A \to ((x \in A ⟼ R) [z] \subseteq y \leftrightarrow (x \in A ⟼ R) [(k, +∞] \cap A] \subseteq y)$
122	119 121	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))$
123	122	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)$
124	49 57 118 123	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)$
125	124	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))$
126	125	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))$
127	32 126	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)$
128	127	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))$
129	24 128	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))$
130	129	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))$
131	20 130	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))$
132	131	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))$
133		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
134		resttopon	$⊢ (ordTop (\leq) \in TopOn (ℝ^{}) \land A \subseteq ℝ^{}) \to ordTop (\leq) ↾_{𝑡} A \in TopOn (A)$
135	133 40 134	sylancr	$⊢ φ \to ordTop (\leq) ↾_{𝑡} A \in TopOn (A)$
136	6 135	eqeltrid	$⊢ φ \to K \in TopOn (A)$
137	5	cnfldtopon	$⊢ J \in TopOn (ℂ)$
138	137	a1i	$⊢ φ \to J \in TopOn (ℂ)$
139		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))))$
140	136 138 14 139	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))))$
141	140	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))))$
142	8 132 141	mpbir2and	$⊢ (φ \land (x \in B ⟼ R) \underset{ℝ}{⇝} C) \to (x \in A ⟼ R) \in (K CnP J) (+∞)$
143		simplr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (x \in A ⟼ R) \in (K CnP J) (+∞)$
144	17	ad2antrr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to C \in ℂ$
145	72	adantl	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to r \in ℝ^{*}$
146	22	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land C \in ℂ \land r \in ℝ^{*}) \to C ball (abs \circ -) r \in J$
147	21 144 145 146	mp3an2i	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to C ball (abs \circ -) r \in J$
148	18	ad2antrr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (x \in A ⟼ R) (+∞) = C$
149		simpr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
150	21 144 149 90	mp3an2i	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to C \in (C ball (abs \circ -) r)$
151	148 150	eqeltrd	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to (x \in A ⟼ R) (+∞) \in (C ball (abs \circ -) r)$
152		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)$
153	143 147 151 152	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)$
154		vex	$⊢ w \in V$
155	154	inex1	$⊢ w \cap A \in V$
156	155	a1i	$⊢ (((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \land w \in ordTop (\leq)) \to w \cap A \in V$
157	6	eleq2i	$⊢ z \in K \leftrightarrow z \in (ordTop (\leq) ↾_{𝑡} A)$
158	43	ad2antrr	$⊢ ((φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \land r \in ℝ^{+}) \to A \in V$
159		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)$
160	33 158 159	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)$
161	157 160	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)$
162		eleq2	$⊢ z = w \cap A \to (+∞ \in z \leftrightarrow +∞ \in (w \cap A))$
163		imaeq2	$⊢ z = w \cap A \to (x \in A ⟼ R) [z] = (x \in A ⟼ R) [w \cap A]$
164	163	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)$
165	162 164	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))$
166	165	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))$
167	156 161 166	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))$
168	153 167	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)$
169		elinel1	$⊢ +∞ \in (w \cap A) \to +∞ \in w$
170		pnfnei	$⊢ (w \in ordTop (\leq) \land +∞ \in w) \to \exists k \in ℝ (k, +∞] \subseteq w$
171	169 170	sylan2	$⊢ (w \in ordTop (\leq) \land +∞ \in (w \cap A)) \to \exists k \in ℝ (k, +∞] \subseteq w$
172		df-ima	$⊢ (x \in A ⟼ R) [w \cap A] = ran ({(x \in A ⟼ R) ↾}_{(w \cap A)})$
173		inss2	$⊢ w \cap A \subseteq A$
174		resmpt	$⊢ w \cap A \subseteq A \to {(x \in A ⟼ R) ↾}_{(w \cap A)} = (x \in (w \cap A) ⟼ R)$
175	173 174	ax-mp	$⊢ {(x \in A ⟼ R) ↾}_{(w \cap A)} = (x \in (w \cap A) ⟼ R)$
176	175	rneqi	$⊢ ran ({(x \in A ⟼ R) ↾}_{(w \cap A)}) = ran (x \in (w \cap A) ⟼ R)$
177	172 176	eqtri	$⊢ (x \in A ⟼ R) [w \cap A] = ran (x \in (w \cap A) ⟼ R)$
178	177	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$
179		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)$
180	178 179	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)$
181	16	adantr	$⊢ (φ \land r \in ℝ^{+}) \to \forall x \in A R \in ℂ$
182		ssralv	$⊢ w \cap A \subseteq A \to (\forall x \in A R \in ℂ \to \forall x \in (w \cap A) R \in ℂ)$
183	173 181 182	mpsyl	$⊢ (φ \land r \in ℝ^{+}) \to \forall x \in (w \cap A) R \in ℂ$
184		eqid	$⊢ (x \in (w \cap A) ⟼ R) = (x \in (w \cap A) ⟼ R)$
185		eleq1	$⊢ z = R \to (z \in (C ball (abs \circ -) r) \leftrightarrow R \in (C ball (abs \circ -) r))$
186	184 185	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))$
187	183 186	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))$
188	187	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))$
189	180 188	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))$
190		simplrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to (k, +∞] \subseteq w$
191	35	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to B \subseteq ℝ^{*}$
192		simprl	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in B$
193	191 192	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in ℝ^{*}$
194		simprr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to k < x$
195		pnfge	$⊢ x \in ℝ^{*} \to x \leq +∞$
196	193 195	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \leq +∞$
197		simplrl	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to k \in ℝ$
198	197	rexrd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to k \in ℝ^{*}$
199	198 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 +∞))$
200	193 194 196 199	mpbir3and	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in (k, +∞]$
201	190 200	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in w$
202	26	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to B \subseteq A$
203	202	sselda	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land x \in B) \to x \in A$
204	203	adantrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in A$
205	201 204	elind	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to x \in (w \cap A)$
206	205	ex	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to ((x \in B \land k < x) \to x \in (w \cap A))$
207	206	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)))$
208	21	a1i	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to abs \circ - \in ∞Met (ℂ)$
209	72	adantl	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℝ^{*}$
210	209	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to r \in ℝ^{*}$
211	17	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to C \in ℂ$
212	28	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \to \forall x \in B R \in ℂ$
213	212	r19.21bi	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land x \in B) \to R \in ℂ$
214	213	adantrr	$⊢ (((φ \land r \in ℝ^{+}) \land (k \in ℝ \land (k, +∞] \subseteq w)) \land (x \in B \land k < x)) \to R \in ℂ$
215	208 210 211 214 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)$
216	214 211 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\|$
217	216	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)$
218	215 217	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)$
219	218	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))$
220	207 219	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))$
221	220	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)))$
222	221	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))$
223	222	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)$
224	223	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)$
225	224	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))$
226	225	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))$
227	226	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)))$
228	189 227	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)))$
229	228	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)))$
230	171 229	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)))$
231	230	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))$
232	231	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))$
233	232	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))$
234	233	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))$
235	168 234	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)$
236	235	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)$
237	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))$
238	237	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))$
239	236 238	mpbird	$⊢ (φ \land (x \in A ⟼ R) \in (K CnP J) (+∞)) \to (x \in B ⟼ R) \underset{ℝ}{⇝} C$
240	142 239	impbida	$⊢ φ \to ((x \in B ⟼ R) \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ R) \in (K CnP J) (+∞))$

Metamath Proof Explorer

Theorem xrlimcnp

Proof