Theorem xrlimcnp 26894

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 7053	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
3	2	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
4		eqid 2729	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
5		xrlimcnp.c	. . . . . . . 8 ⊢ (𝑥 = +∞ → 𝑅 = 𝐶)
6		ssun2 4132	. . . . . . . . . 10 ⊢ {+∞} ⊆ (𝐵 ∪ {+∞})
7		pnfex 11187	. . . . . . . . . . 11 ⊢ +∞ ∈ V
8	7	snid 4616	. . . . . . . . . 10 ⊢ +∞ ∈ {+∞}
9	6, 8	sselii 3934	. . . . . . . . 9 ⊢ +∞ ∈ (𝐵 ∪ {+∞})
10		xrlimcnp.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞}))
11	9, 10	eleqtrrid 2835	. . . . . . . 8 ⊢ (𝜑 → +∞ ∈ 𝐴)
12	5	eleq1d 2813	. . . . . . . . 9 ⊢ (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ))
13	1	ralrimiva 3121	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
14	12, 13, 11	rspcdva 3580	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
15	4, 5, 11, 14	fvmptd3 6957	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
16	15	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
17	16	eleq1d 2813	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 ↔ 𝐶 ∈ 𝑦))
18		cnxmet 24676	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
19		xrlimcnp.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘ℂfld)
20	19	cnfldtopn 24685	. . . . . . . . 9 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
21	20	mopni2 24397	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
22	18, 21	mp3an1 1450	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
23		ssun1 4131	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ (𝐵 ∪ {+∞})
24	23, 10	sseqtrrid 3981	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
25		ssralv 4006	. . . . . . . . . . . 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 15438	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
31		letop 23109	. . . . . . . . . . . . . 14 ⊢ (ordTop‘ ≤ ) ∈ Top
32		xrlimcnp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ⊆ ℝ)
33		ressxr 11178	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℝ*
34	32, 33	sstrdi 3950	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℝ*)
35		pnfxr 11188	. . . . . . . . . . . . . . . . . . . 20 ⊢ +∞ ∈ ℝ*
36	35	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → +∞ ∈ ℝ*)
37	36	snssd 4763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {+∞} ⊆ ℝ*)
38	34, 37	unssd 4145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 ∪ {+∞}) ⊆ ℝ*)
39	10, 38	eqsstrd 3972	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℝ*)
40		xrex 12906	. . . . . . . . . . . . . . . . 17 ⊢ ℝ* ∈ V
41	40	ssex 5263	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ ℝ* → 𝐴 ∈ V)
42	39, 41	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
43	42	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 ∈ V)
44		iocpnfordt 23118	. . . . . . . . . . . . . . 15 ⊢ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
46		elrestr 17350	. . . . . . . . . . . . . 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 2839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾)
50		simprl 770	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ)
51	50	rexrd 11184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*)
52	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ℝ*)
53	50	ltpnfd 13041	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 < +∞)
54		ubioc1 13320	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞))
55	51, 52, 53, 54	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞))
56	11	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ 𝐴)
57	55, 56	elind 4153	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))
58		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ)
59	58	rexrd 11184	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ*)
60		elioc1 13308	. . . . . . . . . . . . . . . . . . . . . . . 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 3937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ)
66		ltle 11222	. . . . . . . . . . . . . . . . . . . . . . 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 12921	. . . . . . . . . . . . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ)
77		elbl3 24296	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
78	69, 73, 74, 76, 77	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
79		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 24674	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
81	76, 74, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
82	81	breq1d 5105	. . . . . . . . . . . . . . . . . . . . . . 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 3141	. . . . . . . . . . . . . . . . . . 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 24317	. . . . . . . . . . . . . . . . . . . . 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 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞)))
94	5	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
95	93, 94	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
96	7, 95	ralsn 4635	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
97	92, 96	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
98		ralunb 4150	. . . . . . . . . . . . . . . . . 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 3294	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
102		ss2rab 4024	. . . . . . . . . . . . . . . 16 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
103	101, 102	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)})
104		incom 4162	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘(,]+∞) ∩ 𝐴) = (𝐴 ∩ (𝑘(,]+∞))
105		dfin5 3913	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∩ (𝑘(,]+∞)) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)}
106	104, 105	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ ((𝑘(,]+∞) ∩ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)}
107	4	mptpreima 6191	. . . . . . . . . . . . . . 15 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}
108	103, 106, 107	3sstr4g 3991	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))
109		funmpt 6524	. . . . . . . . . . . . . . 15 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝑅)
110		inss2 4191	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴
111	2	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
112	111	fdmd 6666	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴)
113	110, 112	sseqtrrid 3981	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅))
114		funimass3 6992	. . . . . . . . . . . . . . 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 3948	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)
119		eleq2 2817	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)))
120		imaeq2 6011	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)))
121	120	sseq1d 3969	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))
122	119, 121	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)))
123	122	rspcev 3579	. . . . . . . . . . . 12 ⊢ ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
124	49, 57, 118, 123	syl12anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
125	124	rexlimdvaa 3131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
126	125	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
127	30, 126	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
128	127	rexlimdvaa 3131	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
129	22, 128	syl5 34	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
130	129	expdimp 452	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (𝐶 ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
131	17, 130	sylbid 240	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
132	131	ralrimiva 3121	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
133		letopon 23108	. . . . . . 7 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
134		resttopon 23064	. . . . . . 7 ⊢ (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ 𝐴 ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
135	133, 39, 134	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
136	48, 135	eqeltrid 2832	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐴))
137	19	cnfldtopon 24686	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
138	137	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘ℂ))
139		iscnp 23140	. . . . 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 24404	. . . . . . . 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 2828	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
152		cnpimaex 23159	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
153	143, 147, 151, 152	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
154		vex 3442	. . . . . . . . 9 ⊢ 𝑤 ∈ V
155	154	inex1 5259	. . . . . . . 8 ⊢ (𝑤 ∩ 𝐴) ∈ V
156	155	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → (𝑤 ∩ 𝐴) ∈ V)
157	48	eleq2i 2820	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
158	42	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V)
159		elrest 17349	. . . . . . . . 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 2817	. . . . . . . . 9 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤 ∩ 𝐴)))
163		imaeq2 6011	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)))
164	163	sseq1d 3969	. . . . . . . . 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 5353	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
168	153, 167	mpbid 232	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
169		elinel1 4154	. . . . . . . . . . 11 ⊢ (+∞ ∈ (𝑤 ∩ 𝐴) → +∞ ∈ 𝑤)
170		pnfnei 23123	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑤) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
171	169, 170	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
172		df-ima 5636	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴))
173		inss2 4191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∩ 𝐴) ⊆ 𝐴
174		resmpt 5992	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅))
175	173, 174	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
176	175	rneqi 5883	. . . . . . . . . . . . . . . 16 ⊢ ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
177	172, 176	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
178	177	sseq1i 3966	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
179		dfss3 3926	. . . . . . . . . . . . . 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 4006	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ))
183	173, 181, 182	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ)
184		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
185		eleq1 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
186	184, 185	ralrnmptw 7032	. . . . . . . . . . . . . . 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 3938	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ ℝ*)
194		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 < 𝑥)
195		pnfge 13050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ* → 𝑥 ≤ +∞)
196	193, 195	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ≤ +∞)
197		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ)
198	197	rexrd 11184	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ*)
199	198, 35, 60	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
200	193, 194, 196, 199	mpbir3and 1343	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞))
201	190, 200	sseldd 3938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝑤)
202	24	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵 ⊆ 𝐴)
203	202	sselda 3937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
204	203	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐴)
205	201, 204	elind 4153	. . . . . . . . . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . . . . . . . . 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 5105	. . . . . . . . . . . . . . . . . . . . . 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 3138	. . . . . . . . . . . . . . . . 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 3142	. . . . . . . . . . . . 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 3130	. . . . . 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 3121	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
237	26, 32, 14	rlim2lt 15422	. . . 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 3044  ∃wrex 3053  {crab 3396  Vcvv 3438   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  {csn 4579   class class class wbr 5095   ↦ cmpt 5176  ^◡ccnv 5622  dom cdm 5623  ran crn 5624   ↾ cres 5625   “ cima 5626   ∘ ccom 5627  Fun wfun 6480  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353  ℂcc 11026  ℝcr 11027  +∞cpnf 11165  ℝ^*cxr 11167   < clt 11168   ≤ cle 11169   − cmin 11365  ℝ⁺crp 12911  (,]cioc 13267  abscabs 15159   ⇝_𝑟 crli 15410   ↾_t crest 17342  TopOpenctopn 17343  ordTopcordt 17421  ∞Metcxmet 21264  ballcbl 21266  ℂ_fldccnfld 21279  Topctop 22796  TopOnctopon 22813   CnP ccnp 23128

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 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-map 8762  df-pm 8763  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fi 9320  df-sup 9351  df-inf 9352  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-div 11796  df-nn 12147  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214  df-8 12215  df-9 12216  df-n0 12403  df-z 12490  df-dec 12610  df-uz 12754  df-q 12868  df-rp 12912  df-xneg 13032  df-xadd 13033  df-xmul 13034  df-ioo 13270  df-ioc 13271  df-ico 13272  df-icc 13273  df-fz 13429  df-seq 13927  df-exp 13987  df-cj 15024  df-re 15025  df-im 15026  df-sqrt 15160  df-abs 15161  df-rlim 15414  df-struct 17076  df-slot 17111  df-ndx 17123  df-base 17139  df-plusg 17192  df-mulr 17193  df-starv 17194  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-rest 17344  df-topn 17345  df-topgen 17365  df-ordt 17423  df-ps 18490  df-tsr 18491  df-psmet 21271  df-xmet 21272  df-met 21273  df-bl 21274  df-mopn 21275  df-cnfld 21280  df-top 22797  df-topon 22814  df-topsp 22836  df-bases 22849  df-cnp 23131  df-xms 24224  df-ms 24225

This theorem is referenced by: (None)