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 ⊢φ→F:A⟶ℂ
ellimc3.a ⊢φ→A⊆ℂ
ellimc3.b ⊢φ→B∈ℂ
Assertion ellimc3 ⊢φ→C∈FlimℂB↔C∈ℂ∧∀x∈ℝ+∃y∈ℝ+∀z∈Az≠B∧z−B<y→F⁡z−C<x

Proof

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