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

Theorem ellimc3 25243
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.
StepHypRef Expression
1 ellimc3.f . . 3 (𝜑𝐹:𝐴⟶ℂ)
2 ellimc3.a . . 3 (𝜑𝐴 ⊆ ℂ)
3 ellimc3.b . . 3 (𝜑𝐵 ∈ ℂ)
4 eqid 2736 . . 3 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
51, 2, 3, 4ellimc2 25241 . 2 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
6 cnxmet 24136 . . . . . . . . 9 (abs ∘ − ) ∈ (∞Met‘ℂ)
7 simplr 767 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ ℂ)
8 simpr 485 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
9 blcntr 23766 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))
106, 7, 8, 9mp3an2i 1466 . . . . . . . 8 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))
11 rpxr 12924 . . . . . . . . . . 11 (𝑥 ∈ ℝ+𝑥 ∈ ℝ*)
1211adantl 482 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ*)
134cnfldtopn 24145 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
1413blopn 23856 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ*) → (𝐶(ball‘(abs ∘ − ))𝑥) ∈ (TopOpen‘ℂfld))
156, 7, 12, 14mp3an2i 1466 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (𝐶(ball‘(abs ∘ − ))𝑥) ∈ (TopOpen‘ℂfld))
16 eleq2 2826 . . . . . . . . . . 11 (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶𝑢𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
17 sseq2 3970 . . . . . . . . . . . . 13 (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
1817anbi2d 629 . . . . . . . . . . . 12 (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
1918rexbidv 3175 . . . . . . . . . . 11 (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
2016, 19imbi12d 344 . . . . . . . . . 10 (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))))
2120rspcv 3577 . . . . . . . . 9 ((𝐶(ball‘(abs ∘ − ))𝑥) ∈ (TopOpen‘ℂfld) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))))
2215, 21syl 17 . . . . . . . 8 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))))
2310, 22mpid 44 . . . . . . 7 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
2413mopni2 23849 . . . . . . . . . . 11 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐵𝑣) → ∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣)
256, 24mp3an1 1448 . . . . . . . . . 10 ((𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐵𝑣) → ∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣)
26 ssrin 4193 . . . . . . . . . . . . 13 ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})))
27 imass2 6054 . . . . . . . . . . . . 13 (((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))))
28 sstr2 3951 . . . . . . . . . . . . 13 ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
2926, 27, 283syl 18 . . . . . . . . . . . 12 ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
3029com12 32 . . . . . . . . . . 11 ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
3130reximdv 3167 . . . . . . . . . 10 ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
3225, 31syl5com 31 . . . . . . . . 9 ((𝑣 ∈ (TopOpen‘ℂfld) ∧ 𝐵𝑣) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
3332impr 455 . . . . . . . 8 ((𝑣 ∈ (TopOpen‘ℂfld) ∧ (𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))
3433rexlimiva 3144 . . . . . . 7 (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))
3523, 34syl6 35 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
3635ralrimdva 3151 . . . . 5 ((𝜑𝐶 ∈ ℂ) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
3713mopni2 23849 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝐶𝑢) → ∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢)
386, 37mp3an1 1448 . . . . . . . . 9 ((𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝐶𝑢) → ∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢)
39 r19.29r 3119 . . . . . . . . . . 11 ((∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑥 ∈ ℝ+ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
403ad3antrrr 728 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ ℂ)
41 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
4241rpxrd 12958 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ*)
4313blopn 23856 . . . . . . . . . . . . . . . . 17 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ*) → (𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂfld))
446, 40, 42, 43mp3an2i 1466 . . . . . . . . . . . . . . . 16 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → (𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂfld))
45 blcntr 23766 . . . . . . . . . . . . . . . . 17 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))
466, 40, 41, 45mp3an2i 1466 . . . . . . . . . . . . . . . 16 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))
47 eleq2 2826 . . . . . . . . . . . . . . . . . . 19 (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐵𝑣𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)))
48 ineq1 4165 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝑣 ∩ (𝐴 ∖ {𝐵})) = ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})))
4948imaeq2d 6013 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))))
5049sseq1d 3975 . . . . . . . . . . . . . . . . . . 19 (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
5147, 50anbi12d 631 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
5251rspcev 3581 . . . . . . . . . . . . . . . . 17 (((𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂfld) ∧ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
5352expr 457 . . . . . . . . . . . . . . . 16 (((𝐵(ball‘(abs ∘ − ))𝑦) ∈ (TopOpen‘ℂfld) ∧ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
5444, 46, 53syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
5554rexlimdva 3152 . . . . . . . . . . . . . 14 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))
56 sstr2 3951 . . . . . . . . . . . . . . . . 17 ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))
5756com12 32 . . . . . . . . . . . . . . . 16 ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))
5857anim2d 612 . . . . . . . . . . . . . . 15 ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → ((𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → (𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
5958reximdv 3167 . . . . . . . . . . . . . 14 ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
6055, 59syl9 77 . . . . . . . . . . . . 13 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
6160impd 411 . . . . . . . . . . . 12 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
6261rexlimdva 3152 . . . . . . . . . . 11 ((𝜑𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ+ ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
6339, 62syl5 34 . . . . . . . . . 10 ((𝜑𝐶 ∈ ℂ) → ((∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
6463expd 416 . . . . . . . . 9 ((𝜑𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
6538, 64syl5 34 . . . . . . . 8 ((𝜑𝐶 ∈ ℂ) → ((𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝐶𝑢) → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
6665expdimp 453 . . . . . . 7 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld)) → (𝐶𝑢 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
6766com23 86 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld)) → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
6867ralrimdva 3151 . . . . 5 ((𝜑𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
6936, 68impbid 211 . . . 4 ((𝜑𝐶 ∈ ℂ) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))
701ad2antrr 724 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝐹:𝐴⟶ℂ)
7170ffund 6672 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → Fun 𝐹)
72 inss2 4189 . . . . . . . . . 10 ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})
73 difss 4091 . . . . . . . . . . 11 (𝐴 ∖ {𝐵}) ⊆ 𝐴
7470fdmd 6679 . . . . . . . . . . 11 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → dom 𝐹 = 𝐴)
7573, 74sseqtrrid 3997 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝐴 ∖ {𝐵}) ⊆ dom 𝐹)
7672, 75sstrid 3955 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹)
77 funimass4 6907 . . . . . . . . 9 ((Fun 𝐹 ∧ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
7871, 76, 77syl2anc 584 . . . . . . . 8 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
796a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (abs ∘ − ) ∈ (∞Met‘ℂ))
80 simplrr 776 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ+)
8180rpxrd 12958 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ*)
823ad3antrrr 728 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
8373, 2sstrid 3955 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
8483ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝐴 ∖ {𝐵}) ⊆ ℂ)
8584sselda 3944 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ)
86 elbl3 23745 . . . . . . . . . . . . 13 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℝ*) ∧ (𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦))
8779, 81, 82, 85, 86syl22anc 837 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦))
88 eqid 2736 . . . . . . . . . . . . . . 15 (abs ∘ − ) = (abs ∘ − )
8988cnmetdval 24134 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧𝐵)))
9085, 82, 89syl2anc 584 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧𝐵)))
9190breq1d 5115 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧(abs ∘ − )𝐵) < 𝑦 ↔ (abs‘(𝑧𝐵)) < 𝑦))
9287, 91bitrd 278 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (abs‘(𝑧𝐵)) < 𝑦))
93 simplrl 775 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ+)
9493rpxrd 12958 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ*)
95 simpllr 774 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐶 ∈ ℂ)
96 eldifi 4086 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧𝐴)
97 ffvelcdm 7032 . . . . . . . . . . . . . 14 ((𝐹:𝐴⟶ℂ ∧ 𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
9870, 96, 97syl2an 596 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹𝑧) ∈ ℂ)
99 elbl3 23745 . . . . . . . . . . . . 13 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ (𝐹𝑧) ∈ ℂ)) → ((𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹𝑧)(abs ∘ − )𝐶) < 𝑥))
10079, 94, 95, 98, 99syl22anc 837 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹𝑧)(abs ∘ − )𝐶) < 𝑥))
10188cnmetdval 24134 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹𝑧) − 𝐶)))
10298, 95, 101syl2anc 584 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹𝑧) − 𝐶)))
103102breq1d 5115 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹𝑧)(abs ∘ − )𝐶) < 𝑥 ↔ (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))
104100, 103bitrd 278 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))
10592, 104imbi12d 344 . . . . . . . . . 10 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
106105ralbidva 3172 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (∀𝑧 ∈ (𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
107 elin 3926 . . . . . . . . . . . . 13 (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})))
108107biancomi 463 . . . . . . . . . . . 12 (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)))
109108imbi1i 349 . . . . . . . . . . 11 ((𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
110 impexp 451 . . . . . . . . . . 11 (((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))))
111109, 110bitr2i 275 . . . . . . . . . 10 ((𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) ↔ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))
112111ralbii2 3092 . . . . . . . . 9 (∀𝑧 ∈ (𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))
113 impexp 451 . . . . . . . . . . 11 (((𝑧𝐴𝑧𝐵) → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧𝐴 → (𝑧𝐵 → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
114 eldifsn 4747 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧𝐴𝑧𝐵))
115114imbi1i 349 . . . . . . . . . . 11 ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ ((𝑧𝐴𝑧𝐵) → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
116 impexp 451 . . . . . . . . . . . 12 (((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ (𝑧𝐵 → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
117116imbi2i 335 . . . . . . . . . . 11 ((𝑧𝐴 → ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧𝐴 → (𝑧𝐵 → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
118113, 115, 1173bitr4i 302 . . . . . . . . . 10 ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧𝐴 → ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
119118ralbii2 3092 . . . . . . . . 9 (∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧𝐵)) < 𝑦 → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))
120106, 112, 1193bitr3g 312 . . . . . . . 8 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
12178, 120bitrd 278 . . . . . . 7 (((𝜑𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
122121anassrs 468 . . . . . 6 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
123122rexbidva 3173 . . . . 5 (((𝜑𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
124123ralbidva 3172 . . . 4 ((𝜑𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
12569, 124bitrd 278 . . 3 ((𝜑𝐶 ∈ ℂ) → (∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
126125pm5.32da 579 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝐶𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐵𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
1275, 126bitrd 278 1 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  cdif 3907  cin 3909  wss 3910  {csn 4586   class class class wbr 5105  dom cdm 5633  cima 5636  ccom 5637  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  *cxr 11188   < clt 11189  cmin 11385  +crp 12915  abscabs 15119  TopOpenctopn 17303  ∞Metcxmet 20781  ballcbl 20783  fldccnfld 20796   lim climc 25226
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-fz 13425  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-struct 17019  df-slot 17054  df-ndx 17066  df-base 17084  df-plusg 17146  df-mulr 17147  df-starv 17148  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-rest 17304  df-topn 17305  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cnp 22579  df-xms 23673  df-ms 23674  df-limc 25230
This theorem is referenced by:  dveflem  25343  dvferm1  25349  dvferm2  25351  lhop1  25378  ftc1lem6  25405  ulmdvlem3  25761  unblimceq0  34970  ftc1cnnc  36150  mullimc  43847  ellimcabssub0  43848  limcdm0  43849  mullimcf  43854  constlimc  43855  idlimc  43857  limcperiod  43859  limcrecl  43860  limcleqr  43875  neglimc  43878  addlimc  43879  0ellimcdiv  43880  limclner  43882  fperdvper  44150  ioodvbdlimc1lem2  44163  ioodvbdlimc2lem  44165
  Copyright terms: Public domain W3C validator