Theorem xrlimcnp 26935

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +∞. Since any ⇝_𝑟 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.)

Hypotheses

Ref	Expression
xrlimcnp.a	⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞}))
xrlimcnp.b	⊢ (𝜑 → 𝐵 ⊆ ℝ)
xrlimcnp.r	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ)
xrlimcnp.c	⊢ (𝑥 = +∞ → 𝑅 = 𝐶)
xrlimcnp.j	⊢ 𝐽 = (TopOpen‘ℂfld)
xrlimcnp.k	⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)

Assertion

Ref	Expression
xrlimcnp	⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))

Distinct variable groups:   𝑥,𝐵   𝜑,𝑥   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝑅(𝑥)   𝐽(𝑥)   𝐾(𝑥)

Proof of Theorem xrlimcnp

Dummy variables 𝑘 𝑟 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrlimcnp.r	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ)
2	1	fmpttd 7110	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
3	2	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
4		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
5		xrlimcnp.c	. . . . . . . 8 ⊢ (𝑥 = +∞ → 𝑅 = 𝐶)
6		ssun2 4159	. . . . . . . . . 10 ⊢ {+∞} ⊆ (𝐵 ∪ {+∞})
7		pnfex 11293	. . . . . . . . . . 11 ⊢ +∞ ∈ V
8	7	snid 4643	. . . . . . . . . 10 ⊢ +∞ ∈ {+∞}
9	6, 8	sselii 3960	. . . . . . . . 9 ⊢ +∞ ∈ (𝐵 ∪ {+∞})
10		xrlimcnp.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞}))
11	9, 10	eleqtrrid 2842	. . . . . . . 8 ⊢ (𝜑 → +∞ ∈ 𝐴)
12	5	eleq1d 2820	. . . . . . . . 9 ⊢ (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ))
13	1	ralrimiva 3133	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
14	12, 13, 11	rspcdva 3607	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
15	4, 5, 11, 14	fvmptd3 7014	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
16	15	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
17	16	eleq1d 2820	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 ↔ 𝐶 ∈ 𝑦))
18		cnxmet 24716	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
19		xrlimcnp.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘ℂfld)
20	19	cnfldtopn 24725	. . . . . . . . 9 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
21	20	mopni2 24437	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
22	18, 21	mp3an1 1450	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
23		ssun1 4158	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ (𝐵 ∪ {+∞})
24	23, 10	sseqtrrid 4007	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
25		ssralv 4032	. . . . . . . . . . . 12 ⊢ (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ))
26	24, 13, 25	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
27	26	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
28		simprl 770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
29		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶)
30	27, 28, 29	rlimi 15534	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
31		letop 23149	. . . . . . . . . . . . . 14 ⊢ (ordTop‘ ≤ ) ∈ Top
32		xrlimcnp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ⊆ ℝ)
33		ressxr 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℝ*
34	32, 33	sstrdi 3976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℝ*)
35		pnfxr 11294	. . . . . . . . . . . . . . . . . . . 20 ⊢ +∞ ∈ ℝ*
36	35	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → +∞ ∈ ℝ*)
37	36	snssd 4790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {+∞} ⊆ ℝ*)
38	34, 37	unssd 4172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 ∪ {+∞}) ⊆ ℝ*)
39	10, 38	eqsstrd 3998	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℝ*)
40		xrex 13008	. . . . . . . . . . . . . . . . 17 ⊢ ℝ* ∈ V
41	40	ssex 5296	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ ℝ* → 𝐴 ∈ V)
42	39, 41	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
43	42	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 ∈ V)
44		iocpnfordt 23158	. . . . . . . . . . . . . . 15 ⊢ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
46		elrestr 17447	. . . . . . . . . . . . . 14 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
47	31, 43, 45, 46	mp3an2i 1468	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
48		xrlimcnp.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)
49	47, 48	eleqtrrdi 2846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾)
50		simprl 770	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ)
51	50	rexrd 11290	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*)
52	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ℝ*)
53	50	ltpnfd 13142	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 < +∞)
54		ubioc1 13421	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞))
55	51, 52, 53, 54	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞))
56	11	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ 𝐴)
57	55, 56	elind 4180	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))
58		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ)
59	58	rexrd 11290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ*)
60		elioc1 13409	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
61	59, 35, 60	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
62		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞) → 𝑘 < 𝑥)
63	61, 62	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 < 𝑥))
64	32	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ)
65	64	sselda 3963	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ)
66		ltle 11328	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥))
67	58, 65, 66	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥))
68	63, 67	syld 47	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 ≤ 𝑥))
69	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
70		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
71	70	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ+)
72		rpxr 13023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ*)
74	14	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)
75	26	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
76	75	r19.21bi 3238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ)
77		elbl3 24336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
78	69, 73, 74, 76, 77	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
79		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 24714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
81	76, 74, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
82	81	breq1d 5134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟))
83	78, 82	bitrd 279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟))
84	83	biimprd 248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((abs‘(𝑅 − 𝐶)) < 𝑟 → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
85	68, 84	imim12d 81	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
86	85	ralimdva 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → (∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
87	86	impr 454	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
88	14	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ ℂ)
89		simplrl 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑟 ∈ ℝ+)
90		blcntr 24357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
91	18, 88, 89, 90	mp3an2i 1468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
92	91	a1d 25	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
93		eleq1 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞)))
94	5	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
95	93, 94	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
96	7, 95	ralsn 4662	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
97	92, 96	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
98		ralunb 4177	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
99	87, 97, 98	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
100	10	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 = (𝐵 ∪ {+∞}))
101	99, 100	raleqtrrdv 3313	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
102		ss2rab 4051	. . . . . . . . . . . . . . . 16 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
103	101, 102	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)})
104		incom 4189	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘(,]+∞) ∩ 𝐴) = (𝐴 ∩ (𝑘(,]+∞))
105		dfin5 3939	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∩ (𝑘(,]+∞)) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)}
106	104, 105	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ ((𝑘(,]+∞) ∩ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)}
107	4	mptpreima 6232	. . . . . . . . . . . . . . 15 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}
108	103, 106, 107	3sstr4g 4017	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))
109		funmpt 6579	. . . . . . . . . . . . . . 15 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝑅)
110		inss2 4218	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴
111	2	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
112	111	fdmd 6721	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴)
113	110, 112	sseqtrrid 4007	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅))
114		funimass3 7049	. . . . . . . . . . . . . . 15 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝑅) ∧ ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
115	109, 113, 114	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
116	108, 115	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
117		simplrr 777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
118	116, 117	sstrd 3974	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)
119		eleq2 2824	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)))
120		imaeq2 6048	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)))
121	120	sseq1d 3995	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))
122	119, 121	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)))
123	122	rspcev 3606	. . . . . . . . . . . 12 ⊢ ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
124	49, 57, 118, 123	syl12anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
125	124	rexlimdvaa 3143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
126	125	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
127	30, 126	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
128	127	rexlimdvaa 3143	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
129	22, 128	syl5 34	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
130	129	expdimp 452	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (𝐶 ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
131	17, 130	sylbid 240	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
132	131	ralrimiva 3133	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
133		letopon 23148	. . . . . . 7 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
134		resttopon 23104	. . . . . . 7 ⊢ (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ 𝐴 ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
135	133, 39, 134	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
136	48, 135	eqeltrid 2839	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐴))
137	19	cnfldtopon 24726	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
138	137	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘ℂ))
139		iscnp 23180	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝐴) ∧ 𝐽 ∈ (TopOn‘ℂ) ∧ +∞ ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))))
140	136, 138, 11, 139	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))))
141	140	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))))
142	3, 132, 141	mpbir2and 713	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
143		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
144	14	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ ℂ)
145	72	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
146	20	blopn 24444	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
147	18, 144, 145, 146	mp3an2i 1468	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
148	15	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
149		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ+)
150	18, 144, 149, 90	mp3an2i 1468	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
151	148, 150	eqeltrd 2835	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
152		cnpimaex 23199	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
153	143, 147, 151, 152	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
154		vex 3468	. . . . . . . . 9 ⊢ 𝑤 ∈ V
155	154	inex1 5292	. . . . . . . 8 ⊢ (𝑤 ∩ 𝐴) ∈ V
156	155	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → (𝑤 ∩ 𝐴) ∈ V)
157	48	eleq2i 2827	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
158	42	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V)
159		elrest 17446	. . . . . . . . 9 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴)))
160	31, 158, 159	sylancr 587	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴)))
161	157, 160	bitrid 283	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ 𝐾 ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴)))
162		eleq2 2824	. . . . . . . . 9 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤 ∩ 𝐴)))
163		imaeq2 6048	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)))
164	163	sseq1d 3995	. . . . . . . . 9 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
165	162, 164	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
166	165	adantl 481	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 = (𝑤 ∩ 𝐴)) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
167	156, 161, 166	rexxfr2d 5386	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
168	153, 167	mpbid 232	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
169		elinel1 4181	. . . . . . . . . . 11 ⊢ (+∞ ∈ (𝑤 ∩ 𝐴) → +∞ ∈ 𝑤)
170		pnfnei 23163	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑤) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
171	169, 170	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
172		df-ima 5672	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴))
173		inss2 4218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∩ 𝐴) ⊆ 𝐴
174		resmpt 6029	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅))
175	173, 174	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
176	175	rneqi 5922	. . . . . . . . . . . . . . . 16 ⊢ ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
177	172, 176	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
178	177	sseq1i 3992	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
179		dfss3 3952	. . . . . . . . . . . . . 14 ⊢ (ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
180	178, 179	bitri 275	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
181	13	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
182		ssralv 4032	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ))
183	173, 181, 182	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ)
184		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
185		eleq1 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
186	184, 185	ralrnmptw 7089	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
187	183, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
188	187	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
189	180, 188	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
190		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑘(,]+∞) ⊆ 𝑤)
191	34	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐵 ⊆ ℝ*)
192		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐵)
193	191, 192	sseldd 3964	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ ℝ*)
194		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 < 𝑥)
195		pnfge 13151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ* → 𝑥 ≤ +∞)
196	193, 195	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ≤ +∞)
197		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ)
198	197	rexrd 11290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ*)
199	198, 35, 60	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
200	193, 194, 196, 199	mpbir3and 1343	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞))
201	190, 200	sseldd 3964	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝑤)
202	24	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵 ⊆ 𝐴)
203	202	sselda 3963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
204	203	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐴)
205	201, 204	elind 4180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑤 ∩ 𝐴))
206	205	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑥 ∈ (𝑤 ∩ 𝐴)))
207	206	imim1d 82	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
208	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
209	72	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
210	209	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑟 ∈ ℝ*)
211	14	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐶 ∈ ℂ)
212	26	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
213	212	r19.21bi 3238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ)
214	213	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑅 ∈ ℂ)
215	208, 210, 211, 214, 77	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
216	214, 211, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
217	216	breq1d 5134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟))
218	215, 217	bitrd 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟))
219	218	pm5.74da 803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟)))
220	207, 219	sylibd 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟)))
221	220	exp4a 431	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (𝑥 ∈ 𝐵 → (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
222	221	ralimdv2 3150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
223	222	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
224	223	an32s 652	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
225	224	expr 456	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ 𝑘 ∈ ℝ) → ((𝑘(,]+∞) ⊆ 𝑤 → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
226	225	reximdva 3154	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
227	226	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
228	189, 227	syld 47	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
229	228	com23 86	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
230	171, 229	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
231	230	impl 455	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
232	231	expimpd 453	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → ((+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
233	232	rexlimdva 3142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
234	233	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
235	168, 234	mpd 15	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
236	235	ralrimiva 3133	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
237	26, 32, 14	rlim2lt 15518	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
238	237	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
239	236, 238	mpbird 257	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶)
240	142, 239	impbida 800	1 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061  {crab 3420  Vcvv 3464   ∪ cun 3929   ∩ cin 3930   ⊆ wss 3931  {csn 4606   class class class wbr 5124   ↦ cmpt 5206  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   ↾ cres 5661   “ cima 5662   ∘ ccom 5663  Fun wfun 6530  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  ℂcc 11132  ℝcr 11133  +∞cpnf 11271  ℝ^*cxr 11273   < clt 11274   ≤ cle 11275   − cmin 11471  ℝ⁺crp 13013  (,]cioc 13368  abscabs 15258   ⇝_𝑟 crli 15506   ↾_t crest 17439  TopOpenctopn 17440  ordTopcordt 17518  ∞Metcxmet 21305  ballcbl 21307  ℂ_fldccnfld 21320  Topctop 22836  TopOnctopon 22853   CnP ccnp 23168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-pre-sup 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-er 8724  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fi 9428  df-sup 9459  df-inf 9460  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12507  df-z 12594  df-dec 12714  df-uz 12858  df-q 12970  df-rp 13014  df-xneg 13133  df-xadd 13134  df-xmul 13135  df-ioo 13371  df-ioc 13372  df-ico 13373  df-icc 13374  df-fz 13530  df-seq 14025  df-exp 14085  df-cj 15123  df-re 15124  df-im 15125  df-sqrt 15259  df-abs 15260  df-rlim 15510  df-struct 17171  df-slot 17206  df-ndx 17218  df-base 17234  df-plusg 17289  df-mulr 17290  df-starv 17291  df-tset 17295  df-ple 17296  df-ds 17298  df-unif 17299  df-rest 17441  df-topn 17442  df-topgen 17462  df-ordt 17520  df-ps 18581  df-tsr 18582  df-psmet 21312  df-xmet 21313  df-met 21314  df-bl 21315  df-mopn 21316  df-cnfld 21321  df-top 22837  df-topon 22854  df-topsp 22876  df-bases 22889  df-cnp 23171  df-xms 24264  df-ms 24265

This theorem is referenced by: (None)