ellimc3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ellimc3		Structured version Visualization version GIF version

Theorem ellimc3 25851

Description: Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.)

**Hypotheses**
Ref	Expression
ellimc3.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
ellimc3.a	⊢ (𝜑 → 𝐴 ⊆ ℂ)
ellimc3.b	⊢ (𝜑 → 𝐵 ∈ ℂ)

**Assertion**
Ref	Expression
ellimc3	⊢ (𝜑 → (𝐶 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))

Distinct variable groups: 𝑥,𝑦,𝑧,𝐴 𝑥,𝐵,𝑦,𝑧 𝑥,𝐶,𝑦,𝑧 𝜑,𝑥,𝑦,𝑧 𝑥,𝐹,𝑦,𝑧

Proof of Theorem ellimc3 Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ellimc3.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
2		ellimc3.a	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
3		ellimc3.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		eqid 2737	. . 3 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
5	1, 2, 3, 4	ellimc2 25849	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
6		cnxmet 24731	. . . . . . . . 9 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
7		simplr 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
8		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
9		blcntr 24372	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))
10	6, 7, 8, 9	mp3an2i 1469	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))
11		rpxr 12927	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ^*)
12	11	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ^*)
13	4	cnfldtopn 24740	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
14	13	blopn 24459	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ^*) → (𝐶(ball‘(abs ∘ − ))𝑥) ∈ (TopOpen‘ℂ_fld))
15	6, 7, 12, 14	mp3an2i 1469	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (𝐶(ball‘(abs ∘ − ))𝑥) ∈ (TopOpen‘ℂ_fld))
16		eleq2 2826	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
17		sseq2 3962	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
18	17	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
19	18	rexbidv 3162	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
20	16, 19	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))))
21	20	rspcv 3574	. . . . . . . . 9 ⊢ ((𝐶(ball‘(abs ∘ − ))𝑥) ∈ (TopOpen‘ℂ_fld) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))))
22	15, 21	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))))
23	10, 22	mpid 44	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
24	13	mopni2 24452	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂ_fld) ∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ⁺ (𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣)
25	6, 24	mp3an1 1451	. . . . . . . . . 10 ⊢ ((𝑣 ∈ (TopOpen‘ℂ_fld) ∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ⁺ (𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣)
26		ssrin 4196	. . . . . . . . . . . . 13 ⊢ ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})))
27		imass2 6069	. . . . . . . . . . . . 13 ⊢ (((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))))
28		sstr2 3942	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
29	26, 27, 28	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
30	29	com12 32	. . . . . . . . . . 11 ⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
31	30	reximdv 3153	. . . . . . . . . 10 ⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑦 ∈ ℝ⁺ (𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
32	25, 31	syl5com 31	. . . . . . . . 9 ⊢ ((𝑣 ∈ (TopOpen‘ℂ_fld) ∧ 𝐵 ∈ 𝑣) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
33	32	impr 454	. . . . . . . 8 ⊢ ((𝑣 ∈ (TopOpen‘ℂ_fld) ∧ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))
34	33	rexlimiva 3131	. . . . . . 7 ⊢ (∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))
35	23, 34	syl6 35	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
36	35	ralrimdva 3138	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
37	13	mopni2 24452	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂ_fld) ∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ⁺ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢)
38	6, 37	mp3an1 1451	. . . . . . . . 9 ⊢ ((𝑢 ∈ (TopOpen‘ℂ_fld) ∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ⁺ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢)
39		r19.29r 3102	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ ℝ⁺ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑥 ∈ ℝ⁺ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
40	3	ad3antrrr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → 𝐵 ∈ ℂ)
41		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ⁺)
42	41	rpxrd 12962	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ^*)
43	13	blopn 24459	. . . . . . . . . . . . . . . . 17 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ^*) → (𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂ_fld))
44	6, 40, 42, 43	mp3an2i 1469	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → (𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂ_fld))
45		blcntr 24372	. . . . . . . . . . . . . . . . 17 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ⁺) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))
46	6, 40, 41, 45	mp3an2i 1469	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))
47		eleq2 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐵 ∈ 𝑣 ↔ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)))
48		ineq1 4167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝑣 ∩ (𝐴 ∖ {𝐵})) = ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})))
49	48	imaeq2d 6027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))))
50	49	sseq1d 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
51	47, 50	anbi12d 633	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
52	51	rspcev 3578	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂ_fld) ∧ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
53	52	expr 456	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂ_fld) ∧ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
54	44, 46, 53	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
55	54	rexlimdva 3139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
56		sstr2 3942	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))
57	56	com12 32	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))
58	57	anim2d 613	. . . . . . . . . . . . . . 15 ⊢ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
59	58	reximdv 3153	. . . . . . . . . . . . . 14 ⊢ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
60	55, 59	syl9 77	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
61	60	impd 410	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
62	61	rexlimdva 3139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ⁺ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
63	39, 62	syl5 34	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((∃𝑥 ∈ ℝ⁺ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
64	63	expd 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ⁺ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
65	38, 64	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (TopOpen‘ℂ_fld) ∧ 𝐶 ∈ 𝑢) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
66	65	expdimp 452	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂ_fld)) → (𝐶 ∈ 𝑢 → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
67	66	com23 86	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂ_fld)) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
68	67	ralrimdva 3138	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
69	36, 68	impbid 212	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
70	1	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → 𝐹:𝐴⟶ℂ)
71	70	ffund 6674	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → Fun 𝐹)
72		inss2 4192	. . . . . . . . . 10 ⊢ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})
73		difss 4090	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴
74	70	fdmd 6680	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → dom 𝐹 = 𝐴)
75	73, 74	sseqtrrid 3979	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (𝐴 ∖ {𝐵}) ⊆ dom 𝐹)
76	72, 75	sstrid 3947	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹)
77		funimass4 6906	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
78	71, 76, 77	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
79	6	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (abs ∘ − ) ∈ (∞Met‘ℂ))
80		simplrr 778	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ⁺)
81	80	rpxrd 12962	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ^*)
82	3	ad3antrrr 731	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
83	73, 2	sstrid 3947	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
84	83	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (𝐴 ∖ {𝐵}) ⊆ ℂ)
85	84	sselda 3935	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ)
86		elbl3 24351	. . . . . . . . . . . . 13 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℝ^*) ∧ (𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦))
87	79, 81, 82, 85, 86	syl22anc 839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦))
88		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
89	88	cnmetdval 24729	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵)))
90	85, 82, 89	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵)))
91	90	breq1d 5110	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧(abs ∘ − )𝐵) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < 𝑦))
92	87, 91	bitrd 279	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (abs‘(𝑧 − 𝐵)) < 𝑦))
93		simplrl 777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ⁺)
94	93	rpxrd 12962	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ^*)
95		simpllr 776	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐶 ∈ ℂ)
96		eldifi 4085	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ 𝐴)
97		ffvelcdm 7035	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ)
98	70, 96, 97	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ)
99		elbl3 24351	. . . . . . . . . . . . 13 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℝ^*) ∧ (𝐶 ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ)) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥))
100	79, 94, 95, 98, 99	syl22anc 839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥))
101	88	cnmetdval 24729	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑧) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶)))
102	98, 95, 101	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶)))
103	102	breq1d 5110	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥 ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))
104	100, 103	bitrd 279	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))
105	92, 104	imbi12d 344	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
106	105	ralbidva 3159	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (∀𝑧 ∈ (𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
107		elin 3919	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})))
108	107	biancomi 462	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)))
109	108	imbi1i 349	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
110		impexp 450	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))))
111	109, 110	bitr2i 276	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) ↔ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
112	111	ralbii2 3080	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))
113		impexp 450	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
114		eldifsn 4744	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵))
115	114	imbi1i 349	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
116		impexp 450	. . . . . . . . . . . 12 ⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
117	116	imbi2i 336	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
118	113, 115, 117	3bitr4i 303	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
119	118	ralbii2 3080	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))
120	106, 112, 119	3bitr3g 313	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
121	78, 120	bitrd 279	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
122	121	anassrs 467	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑦 ∈ ℝ⁺) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
123	122	rexbidva 3160	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ⁺) → (∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
124	123	ralbidva 3159	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
125	69, 124	bitrd 279	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))
126	125	pm5.32da 579	. 2 ⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂ_fld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈ (TopOpen‘ℂ_fld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
127	5, 126	bitrd 279	1 ⊢ (𝜑 → (𝐶 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∖ cdif 3900 ∩ cin 3902 ⊆ wss 3903 {csn 4582 class class class wbr 5100 dom cdm 5632 “ cima 5635 ∘ ccom 5636 Fun wfun 6494 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ℂcc 11036 ℝ^*cxr 11177 < clt 11178 − cmin 11376 ℝ⁺crp 12917 abscabs 15169 TopOpenctopn 17353 ∞Metcxmet 21309 ballcbl 21311 ℂ_fldccnfld 21324 lim_ℂ climc 25834

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 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-map 8777 df-pm 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fi 9326 df-sup 9357 df-inf 9358 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-q 12874 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-fz 13436 df-seq 13937 df-exp 13997 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-struct 17086 df-slot 17121 df-ndx 17133 df-base 17149 df-plusg 17202 df-mulr 17203 df-starv 17204 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-rest 17354 df-topn 17355 df-topgen 17375 df-psmet 21316 df-xmet 21317 df-met 21318 df-bl 21319 df-mopn 21320 df-cnfld 21325 df-top 22853 df-topon 22870 df-topsp 22892 df-bases 22905 df-cnp 23187 df-xms 24279 df-ms 24280 df-limc 25838

This theorem is referenced by: dveflem 25954 dvferm1 25960 dvferm2 25962 lhop1 25990 ftc1lem6 26019 ulmdvlem3 26382 unblimceq0 36733 ftc1cnnc 37947 mullimc 45980 ellimcabssub0 45981 limcdm0 45982 mullimcf 45987 constlimc 45988 idlimc 45990 limcperiod 45992 limcrecl 45993 limcleqr 46006 neglimc 46009 addlimc 46010 0ellimcdiv 46011 limclner 46013 fperdvper 46281 ioodvbdlimc1lem2 46294 ioodvbdlimc2lem 46296

W3C validator