This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ellimc3

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

Ref Expression
Hypotheses ellimc3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
ellimc3.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
ellimc3.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion ellimc3 ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 ellimc3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 ellimc3.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 ellimc3.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
5 1 2 3 4 ellimc2 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )
6 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
7 simplr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
9 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) )
10 6 7 8 9 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) )
11 rpxr ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ* )
12 11 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ* )
13 4 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
14 13 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ* ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ∈ ( TopOpen ‘ ℂfld ) )
15 6 7 12 14 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ∈ ( TopOpen ‘ ℂfld ) )
16 eleq2 ⊢ ( 𝑢 = ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( 𝐶 ∈ 𝑢 ↔ 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
17 sseq2 ⊢ ( 𝑢 = ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
18 17 anbi2d ⊢ ( 𝑢 = ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
19 18 rexbidv ⊢ ( 𝑢 = ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
20 16 19 imbi12d ⊢ ( 𝑢 = ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ↔ ( 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) ) )
21 20 rspcv ⊢ ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ∈ ( TopOpen ‘ ℂfld ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ( 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) ) )
22 15 21 syl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ( 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) ) )
23 10 22 mpid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
24 13 mopni2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐵 ∈ 𝑣 ) → ∃ 𝑦 ∈ ℝ+ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ 𝑣 )
25 6 24 mp3an1 ⊢ ( ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐵 ∈ 𝑣 ) → ∃ 𝑦 ∈ ℝ+ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ 𝑣 )
26 ssrin ⊢ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ 𝑣 → ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
27 imass2 ⊢ ( ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) )
28 sstr2 ⊢ ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
29 26 27 28 3syl ⊢ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ 𝑣 → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
30 29 com12 ⊢ ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ 𝑣 → ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
31 30 reximdv ⊢ ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ∃ 𝑦 ∈ ℝ+ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ⊆ 𝑣 → ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
32 25 31 syl5com ⊢ ( ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐵 ∈ 𝑣 ) → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
33 32 impr ⊢ ( ( 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) )
34 33 rexlimiva ⊢ ( ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) )
35 23 34 syl6 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
36 35 ralrimdva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
37 13 mopni2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐶 ∈ 𝑢 ) → ∃ 𝑥 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 )
38 6 37 mp3an1 ⊢ ( ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐶 ∈ 𝑢 ) → ∃ 𝑥 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 )
39 r19.29r ⊢ ( ( ∃ 𝑥 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ∃ 𝑥 ∈ ℝ+ ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 ∧ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
40 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
42 41 rpxrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ* )
43 13 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ* ) → ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∈ ( TopOpen ‘ ℂfld ) )
44 6 40 42 43 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∈ ( TopOpen ‘ ℂfld ) )
45 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ+ ) → 𝐵 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) )
46 6 40 41 45 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐵 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) )
47 eleq2 ⊢ ( 𝑣 = ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐵 ∈ 𝑣 ↔ 𝐵 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) )
48 ineq1 ⊢ ( 𝑣 = ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
49 48 imaeq2d ⊢ ( 𝑣 = ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) = ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) )
50 49 sseq1d ⊢ ( 𝑣 = ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
51 47 50 anbi12d ⊢ ( 𝑣 = ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ↔ ( 𝐵 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∧ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
52 51 rspcev ⊢ ( ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∧ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
53 52 expr ⊢ ( ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐵 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
54 44 46 53 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
55 54 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
56 sstr2 ⊢ ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 → ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
57 56 com12 ⊢ ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
58 57 anim2d ⊢ ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 → ( ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
59 58 reximdv ⊢ ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 → ( ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
60 55 59 syl9 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 → ( ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
61 60 impd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 ∧ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
62 61 rexlimdva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∃ 𝑥 ∈ ℝ+ ( ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 ∧ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
63 39 62 syl5 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( ∃ 𝑥 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
64 63 expd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∃ 𝑥 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ⊆ 𝑢 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
65 38 64 syl5 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝐶 ∈ 𝑢 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
66 65 expdimp ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝐶 ∈ 𝑢 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
67 66 com23 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
68 67 ralrimdva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) → ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
69 36 68 impbid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
70 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → 𝐹 : 𝐴 ⟶ ℂ )
71 70 ffund ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → Fun 𝐹 )
72 inss2 ⊢ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝐴 ∖ { 𝐵 } )
73 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
74 70 fdmd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → dom 𝐹 = 𝐴 )
75 73 74 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ dom 𝐹 )
76 72 75 sstrid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ dom 𝐹 )
77 funimass4 ⊢ ( ( Fun 𝐹 ∧ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∀ 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
78 71 76 77 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∀ 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
79 6 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
80 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑦 ∈ ℝ+ )
81 80 rpxrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑦 ∈ ℝ* )
82 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
83 73 2 sstrid ⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
84 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
85 84 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ℂ )
86 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ↔ ( 𝑧 ( abs ∘ − ) 𝐵 ) < 𝑦 ) )
87 79 81 82 85 86 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ↔ ( 𝑧 ( abs ∘ − ) 𝐵 ) < 𝑦 ) )
88 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
89 88 cnmetdval ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 𝐵 ) = ( abs ‘ ( 𝑧 − 𝐵 ) ) )
90 85 82 89 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 ( abs ∘ − ) 𝐵 ) = ( abs ‘ ( 𝑧 − 𝐵 ) ) )
91 90 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑧 ( abs ∘ − ) 𝐵 ) < 𝑦 ↔ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) )
92 87 91 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ↔ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) )
93 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑥 ∈ ℝ+ )
94 93 rpxrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑥 ∈ ℝ* )
95 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐶 ∈ ℂ )
96 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑧 ∈ 𝐴 )
97 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
98 70 96 97 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
99 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( abs ∘ − ) 𝐶 ) < 𝑥 ) )
100 79 94 95 98 99 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( abs ∘ − ) 𝐶 ) < 𝑥 ) )
101 88 cnmetdval ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑧 ) ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) )
102 98 95 101 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) )
103 102 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) ( abs ∘ − ) 𝐶 ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) )
104 100 103 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) )
105 92 104 imbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ↔ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
106 105 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ↔ ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
107 elin ⊢ ( 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) )
108 107 biancomi ⊢ ( 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) )
109 108 imbi1i ⊢ ( ( 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ↔ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
110 impexp ⊢ ( ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) )
111 109 110 bitr2i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ) ↔ ( 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) )
112 111 ralbii2 ⊢ ( ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ) ↔ ∀ 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) )
113 impexp ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝑧 ∈ 𝐴 → ( 𝑧 ≠ 𝐵 → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )
114 eldifsn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) )
115 114 imbi1i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵 ) → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
116 impexp ⊢ ( ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑧 ≠ 𝐵 → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
117 116 imbi2i ⊢ ( ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝑧 ∈ 𝐴 → ( 𝑧 ≠ 𝐵 → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )
118 113 115 117 3bitr4i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
119 118 ralbii2 ⊢ ( ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) )
120 106 112 119 3bitr3g ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( ∀ 𝑧 ∈ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
121 78 120 bitrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
122 121 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
123 122 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
124 123 ralbidva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ( 𝐹 “ ( ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
125 69 124 bitrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
126 125 pm5.32da ⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )
127 5 126 bitrd ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )