Theorem xrlimcnp 26932

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 7067	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
3	2	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
4		eqid 2736	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
5		xrlimcnp.c	. . . . . . . 8 ⊢ (𝑥 = +∞ → 𝑅 = 𝐶)
6		ssun2 4119	. . . . . . . . . 10 ⊢ {+∞} ⊆ (𝐵 ∪ {+∞})
7		pnfex 11198	. . . . . . . . . . 11 ⊢ +∞ ∈ V
8	7	snid 4606	. . . . . . . . . 10 ⊢ +∞ ∈ {+∞}
9	6, 8	sselii 3918	. . . . . . . . 9 ⊢ +∞ ∈ (𝐵 ∪ {+∞})
10		xrlimcnp.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞}))
11	9, 10	eleqtrrid 2843	. . . . . . . 8 ⊢ (𝜑 → +∞ ∈ 𝐴)
12	5	eleq1d 2821	. . . . . . . . 9 ⊢ (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ))
13	1	ralrimiva 3129	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
14	12, 13, 11	rspcdva 3565	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
15	4, 5, 11, 14	fvmptd3 6971	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
16	15	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
17	16	eleq1d 2821	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 ↔ 𝐶 ∈ 𝑦))
18		cnxmet 24737	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
19		xrlimcnp.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘ℂfld)
20	19	cnfldtopn 24746	. . . . . . . . 9 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
21	20	mopni2 24458	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
22	18, 21	mp3an1 1451	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
23		ssun1 4118	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ (𝐵 ∪ {+∞})
24	23, 10	sseqtrrid 3965	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
25		ssralv 3990	. . . . . . . . . . . 12 ⊢ (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ))
26	24, 13, 25	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
27	26	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
28		simprl 771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
29		simplr 769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶)
30	27, 28, 29	rlimi 15475	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
31		letop 23171	. . . . . . . . . . . . . 14 ⊢ (ordTop‘ ≤ ) ∈ Top
32		xrlimcnp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ⊆ ℝ)
33		ressxr 11189	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℝ*
34	32, 33	sstrdi 3934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ ℝ*)
35		pnfxr 11199	. . . . . . . . . . . . . . . . . . . 20 ⊢ +∞ ∈ ℝ*
36	35	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → +∞ ∈ ℝ*)
37	36	snssd 4730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {+∞} ⊆ ℝ*)
38	34, 37	unssd 4132	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 ∪ {+∞}) ⊆ ℝ*)
39	10, 38	eqsstrd 3956	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℝ*)
40		xrex 12937	. . . . . . . . . . . . . . . . 17 ⊢ ℝ* ∈ V
41	40	ssex 5262	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ ℝ* → 𝐴 ∈ V)
42	39, 41	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ V)
43	42	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 ∈ V)
44		iocpnfordt 23180	. . . . . . . . . . . . . . 15 ⊢ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )
45	44	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
46		elrestr 17391	. . . . . . . . . . . . . 14 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
47	31, 43, 45, 46	mp3an2i 1469	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
48		xrlimcnp.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)
49	47, 48	eleqtrrdi 2847	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾)
50		simprl 771	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ)
51	50	rexrd 11195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*)
52	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ℝ*)
53	50	ltpnfd 13072	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 < +∞)
54		ubioc1 13352	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞))
55	51, 52, 53, 54	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞))
56	11	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ 𝐴)
57	55, 56	elind 4140	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))
58		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ)
59	58	rexrd 11195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ*)
60		elioc1 13340	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
61	59, 35, 60	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
62		simp2 1138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞) → 𝑘 < 𝑥)
63	61, 62	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 < 𝑥))
64	32	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ)
65	64	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ)
66		ltle 11234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥))
67	58, 65, 66	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥))
68	63, 67	syld 47	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 ≤ 𝑥))
69	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
70		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
71	70	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ+)
72		rpxr 12952	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ*)
74	14	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)
75	26	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
76	75	r19.21bi 3229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ)
77		elbl3 24357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
78	69, 73, 74, 76, 77	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
79		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 24735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
81	76, 74, 80	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
82	81	breq1d 5095	. . . . . . . . . . . . . . . . . . . . . . 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 3149	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → (∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
87	86	impr 454	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
88	14	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ ℂ)
89		simplrl 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑟 ∈ ℝ+)
90		blcntr 24378	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
91	18, 88, 89, 90	mp3an2i 1469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
92	91	a1d 25	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
93		eleq1 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞)))
94	5	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
95	93, 94	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
96	7, 95	ralsn 4625	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
97	92, 96	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
98		ralunb 4137	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
99	87, 97, 98	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
100	10	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 = (𝐵 ∪ {+∞}))
101	99, 100	raleqtrrdv 3299	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
102	101	ss2rabd 4012	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)})
103		dfin5 3897	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∩ (𝑘(,]+∞)) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)}
104	103	ineqcomi 4151	. . . . . . . . . . . . . . 15 ⊢ ((𝑘(,]+∞) ∩ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)}
105	4	mptpreima 6202	. . . . . . . . . . . . . . 15 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}
106	102, 104, 105	3sstr4g 3975	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))
107		funmpt 6536	. . . . . . . . . . . . . . 15 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝑅)
108		inss2 4178	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴
109	2	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
110	109	fdmd 6678	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴)
111	108, 110	sseqtrrid 3965	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅))
112		funimass3 7006	. . . . . . . . . . . . . . 15 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝑅) ∧ ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
113	107, 111, 112	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
114	106, 113	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
115		simplrr 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
116	114, 115	sstrd 3932	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)
117		eleq2 2825	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)))
118		imaeq2 6021	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)))
119	118	sseq1d 3953	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))
120	117, 119	anbi12d 633	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)))
121	120	rspcev 3564	. . . . . . . . . . . 12 ⊢ ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
122	49, 57, 116, 121	syl12anc 837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
123	122	rexlimdvaa 3139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
124	123	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
125	30, 124	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))
126	125	rexlimdvaa 3139	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
127	22, 126	syl5 34	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
128	127	expdimp 452	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (𝐶 ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
129	17, 128	sylbid 240	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
130	129	ralrimiva 3129	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))
131		letopon 23170	. . . . . . 7 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
132		resttopon 23126	. . . . . . 7 ⊢ (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ 𝐴 ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
133	131, 39, 132	sylancr 588	. . . . . 6 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
134	48, 133	eqeltrid 2840	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐴))
135	19	cnfldtopon 24747	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
136	135	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘ℂ))
137		iscnp 23202	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝐴) ∧ 𝐽 ∈ (TopOn‘ℂ) ∧ +∞ ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))))
138	134, 136, 11, 137	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))))
139	138	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)))))
140	3, 130, 139	mpbir2and 714	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
141		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
142	14	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ ℂ)
143	72	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
144	20	blopn 24465	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
145	18, 142, 143, 144	mp3an2i 1469	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
146	15	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶)
147		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ+)
148	18, 142, 147, 90	mp3an2i 1469	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
149	146, 148	eqeltrd 2836	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
150		cnpimaex 23221	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
151	141, 145, 149, 150	syl3anc 1374	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
152		vex 3433	. . . . . . . . 9 ⊢ 𝑤 ∈ V
153	152	inex1 5258	. . . . . . . 8 ⊢ (𝑤 ∩ 𝐴) ∈ V
154	153	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → (𝑤 ∩ 𝐴) ∈ V)
155	48	eleq2i 2828	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
156	42	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V)
157		elrest 17390	. . . . . . . . 9 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴)))
158	31, 156, 157	sylancr 588	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴)))
159	155, 158	bitrid 283	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ 𝐾 ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴)))
160		eleq2 2825	. . . . . . . . 9 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤 ∩ 𝐴)))
161		imaeq2 6021	. . . . . . . . . 10 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)))
162	161	sseq1d 3953	. . . . . . . . 9 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
163	160, 162	anbi12d 633	. . . . . . . 8 ⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
164	163	adantl 481	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 = (𝑤 ∩ 𝐴)) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
165	154, 159, 164	rexxfr2d 5353	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
166	151, 165	mpbid 232	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
167		elinel1 4141	. . . . . . . . . . 11 ⊢ (+∞ ∈ (𝑤 ∩ 𝐴) → +∞ ∈ 𝑤)
168		pnfnei 23185	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑤) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
169	167, 168	sylan2 594	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
170		df-ima 5644	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴))
171		inss2 4178	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∩ 𝐴) ⊆ 𝐴
172		resmpt 6002	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅))
173	171, 172	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
174	173	rneqi 5892	. . . . . . . . . . . . . . . 16 ⊢ ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
175	170, 174	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
176	175	sseq1i 3950	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
177		dfss3 3910	. . . . . . . . . . . . . 14 ⊢ (ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
178	176, 177	bitri 275	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
179	13	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
180		ssralv 3990	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ))
181	171, 179, 180	mpsyl 68	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ)
182		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)
183		eleq1 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
184	182, 183	ralrnmptw 7046	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
185	181, 184	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
186	185	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
187	178, 186	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
188		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑘(,]+∞) ⊆ 𝑤)
189	34	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐵 ⊆ ℝ*)
190		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐵)
191	189, 190	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ ℝ*)
192		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 < 𝑥)
193	191	pnfged 13082	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ≤ +∞)
194		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ)
195	194	rexrd 11195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ*)
196	195, 35, 60	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞)))
197	191, 192, 193, 196	mpbir3and 1344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞))
198	188, 197	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝑤)
199	24	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵 ⊆ 𝐴)
200	199	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴)
201	200	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐴)
202	198, 201	elind 4140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑤 ∩ 𝐴))
203	202	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑥 ∈ (𝑤 ∩ 𝐴)))
204	203	imim1d 82	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
205	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
206	72	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
207	206	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑟 ∈ ℝ*)
208	14	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐶 ∈ ℂ)
209	26	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)
210	209	r19.21bi 3229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ)
211	210	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑅 ∈ ℂ)
212	205, 207, 208, 211, 77	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
213	211, 208, 80	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
214	213	breq1d 5095	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟))
215	212, 214	bitrd 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟))
216	215	pm5.74da 804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟)))
217	204, 216	sylibd 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟)))
218	217	exp4a 431	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (𝑥 ∈ 𝐵 → (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
219	218	ralimdv2 3146	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
220	219	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
221	220	an32s 653	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
222	221	expr 456	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ 𝑘 ∈ ℝ) → ((𝑘(,]+∞) ⊆ 𝑤 → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
223	222	reximdva 3150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
224	223	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
225	187, 224	syld 47	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
226	225	com23 86	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
227	169, 226	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))))
228	227	impl 455	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) ∧ +∞ ∈ (𝑤 ∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
229	228	expimpd 453	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → ((+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
230	229	rexlimdva 3138	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
231	230	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
232	166, 231	mpd 15	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
233	232	ralrimiva 3129	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))
234	26, 32, 14	rlim2lt 15459	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
235	234	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))
236	233, 235	mpbird 257	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶)
237	140, 236	impbida 801	1 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429   ∪ cun 3887   ∩ cin 3888   ⊆ wss 3889  {csn 4567   class class class wbr 5085   ↦ cmpt 5166  ^◡ccnv 5630  dom cdm 5631  ran crn 5632   ↾ cres 5633   “ cima 5634   ∘ ccom 5635  Fun wfun 6492  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367  ℂcc 11036  ℝcr 11037  +∞cpnf 11176  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180   − cmin 11377  ℝ⁺crp 12942  (,]cioc 13299  abscabs 15196   ⇝_𝑟 crli 15447   ↾_t crest 17383  TopOpenctopn 17384  ordTopcordt 17463  ∞Metcxmet 21337  ballcbl 21339  ℂ_fldccnfld 21352  Topctop 22858  TopOnctopon 22875   CnP ccnp 23190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fi 9324  df-sup 9355  df-inf 9356  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ioo 13302  df-ioc 13303  df-ico 13304  df-icc 13305  df-fz 13462  df-seq 13964  df-exp 14024  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-rlim 15451  df-struct 17117  df-slot 17152  df-ndx 17164  df-base 17180  df-plusg 17233  df-mulr 17234  df-starv 17235  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-rest 17385  df-topn 17386  df-topgen 17406  df-ordt 17465  df-ps 18532  df-tsr 18533  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-mopn 21348  df-cnfld 21353  df-top 22859  df-topon 22876  df-topsp 22898  df-bases 22911  df-cnp 23193  df-xms 24285  df-ms 24286

This theorem is referenced by: (None)