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

Metamath Proof Explorer

Theorem xrlimcnp

Proof