ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ellimc3apf GIF version

Theorem ellimc3apf 12704
Description: Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
Hypotheses
Ref Expression
ellimc3.f (𝜑𝐹:𝐴⟶ℂ)
ellimc3.a (𝜑𝐴 ⊆ ℂ)
ellimc3.b (𝜑𝐵 ∈ ℂ)
ellimc3.nf 𝑧𝐹
Assertion
Ref Expression
ellimc3apf (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
Distinct variable groups:   𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐹,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑥,𝑦)   𝐹(𝑧)

Proof of Theorem ellimc3apf
Dummy variables 𝑓 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnex 7708 . . . . . . 7 ℂ ∈ V
21a1i 9 . . . . . 6 (𝜑 → ℂ ∈ V)
3 ellimc3.f . . . . . 6 (𝜑𝐹:𝐴⟶ℂ)
4 ellimc3.a . . . . . 6 (𝜑𝐴 ⊆ ℂ)
5 elpm2r 6526 . . . . . 6 (((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm ℂ))
62, 2, 3, 4, 5syl22anc 1200 . . . . 5 (𝜑𝐹 ∈ (ℂ ↑pm ℂ))
7 ellimc3.b . . . . 5 (𝜑𝐵 ∈ ℂ)
81rabex 4040 . . . . . 6 {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ∈ V
98a1i 9 . . . . 5 (𝜑 → {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ∈ V)
10 simpl 108 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → 𝑓 = 𝐹)
1110dmeqd 4709 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → dom 𝑓 = dom 𝐹)
1210, 11feq12d 5230 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑓:dom 𝑓⟶ℂ ↔ 𝐹:dom 𝐹⟶ℂ))
1311sseq1d 3094 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (dom 𝑓 ⊆ ℂ ↔ dom 𝐹 ⊆ ℂ))
1412, 13anbi12d 462 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝐵) → ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ)))
15 simpr 109 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → 𝑤 = 𝐵)
1615eleq1d 2184 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑤 ∈ ℂ ↔ 𝐵 ∈ ℂ))
17 nfcv 2256 . . . . . . . . . . . . . 14 𝑧dom 𝑓
18 ellimc3.nf . . . . . . . . . . . . . . 15 𝑧𝐹
1918nfdm 4751 . . . . . . . . . . . . . 14 𝑧dom 𝐹
2017, 19raleqf 2597 . . . . . . . . . . . . 13 (dom 𝑓 = dom 𝐹 → (∀𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))
2111, 20syl 14 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))
2218nfeq2 2268 . . . . . . . . . . . . . 14 𝑧 𝑓 = 𝐹
23 nfv 1491 . . . . . . . . . . . . . 14 𝑧 𝑤 = 𝐵
2422, 23nfan 1527 . . . . . . . . . . . . 13 𝑧(𝑓 = 𝐹𝑤 = 𝐵)
2515breq2d 3909 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑧 # 𝑤𝑧 # 𝐵))
2615oveq2d 5756 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑧𝑤) = (𝑧𝐵))
2726fveq2d 5391 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝐹𝑤 = 𝐵) → (abs‘(𝑧𝑤)) = (abs‘(𝑧𝐵)))
2827breq1d 3907 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑤 = 𝐵) → ((abs‘(𝑧𝑤)) < 𝑦 ↔ (abs‘(𝑧𝐵)) < 𝑦))
2925, 28anbi12d 462 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑤 = 𝐵) → ((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) ↔ (𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦)))
3010fveq1d 5389 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝐹𝑤 = 𝐵) → (𝑓𝑧) = (𝐹𝑧))
3130fvoveq1d 5762 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑤 = 𝐵) → (abs‘((𝑓𝑧) − 𝑢)) = (abs‘((𝐹𝑧) − 𝑢)))
3231breq1d 3907 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑤 = 𝐵) → ((abs‘((𝑓𝑧) − 𝑢)) < 𝑥 ↔ (abs‘((𝐹𝑧) − 𝑢)) < 𝑥))
3329, 32imbi12d 233 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑤 = 𝐵) → (((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3424, 33ralbid 2410 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3521, 34bitrd 187 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3635rexbidv 2413 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝐵) → (∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3736ralbidv 2412 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝐵) → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))
3816, 37anbi12d 462 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝐵) → ((𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)) ↔ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥))))
3914, 38anbi12d 462 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝐵) → (((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥))) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))))
4039rabbidv 2647 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝐵) → {𝑢 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))} = {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))})
41 df-limced 12700 . . . . . 6 lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑤 ∈ ℂ ↦ {𝑢 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑤 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑤 ∧ (abs‘(𝑧𝑤)) < 𝑦) → (abs‘((𝑓𝑧) − 𝑢)) < 𝑥)))})
4240, 41ovmpoga 5866 . . . . 5 ((𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝐵 ∈ ℂ ∧ {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ∈ V) → (𝐹 lim 𝐵) = {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))})
436, 7, 9, 42syl3anc 1199 . . . 4 (𝜑 → (𝐹 lim 𝐵) = {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))})
4443eleq2d 2185 . . 3 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ 𝐶 ∈ {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))}))
45 oveq2 5748 . . . . . . . . . . . 12 (𝑢 = 𝐶 → ((𝐹𝑧) − 𝑢) = ((𝐹𝑧) − 𝐶))
4645fveq2d 5391 . . . . . . . . . . 11 (𝑢 = 𝐶 → (abs‘((𝐹𝑧) − 𝑢)) = (abs‘((𝐹𝑧) − 𝐶)))
4746breq1d 3907 . . . . . . . . . 10 (𝑢 = 𝐶 → ((abs‘((𝐹𝑧) − 𝑢)) < 𝑥 ↔ (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))
4847imbi2d 229 . . . . . . . . 9 (𝑢 = 𝐶 → (((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
4948ralbidv 2412 . . . . . . . 8 (𝑢 = 𝐶 → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
5049rexbidv 2413 . . . . . . 7 (𝑢 = 𝐶 → (∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
5150ralbidv 2412 . . . . . 6 (𝑢 = 𝐶 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
5251anbi2d 457 . . . . 5 (𝑢 = 𝐶 → ((𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)) ↔ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
5352anbi2d 457 . . . 4 (𝑢 = 𝐶 → (((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥))) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
5453elrab 2811 . . 3 (𝐶 ∈ {𝑢 ∈ ℂ ∣ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝑢)) < 𝑥)))} ↔ (𝐶 ∈ ℂ ∧ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
5544, 54syl6bb 195 . 2 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))))
567biantrurd 301 . . . 4 (𝜑 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
573fdmd 5247 . . . . . . 7 (𝜑 → dom 𝐹 = 𝐴)
5857feq2d 5228 . . . . . 6 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐴⟶ℂ))
593, 58mpbird 166 . . . . 5 (𝜑𝐹:dom 𝐹⟶ℂ)
6057, 4eqsstrd 3101 . . . . 5 (𝜑 → dom 𝐹 ⊆ ℂ)
61 ibar 297 . . . . 5 ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) → ((𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
6259, 60, 61syl2anc 406 . . . 4 (𝜑 → ((𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
6356, 62bitrd 187 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))))
6463anbi2d 457 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝐶 ∈ ℂ ∧ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ) ∧ (𝐵 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))))
65 nfcv 2256 . . . . . . 7 𝑧𝐴
6619, 65raleqf 2597 . . . . . 6 (dom 𝐹 = 𝐴 → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
6757, 66syl 14 . . . . 5 (𝜑 → (∀𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
6867rexbidv 2413 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
6968ralbidv 2412 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)))
7069anbi2d 457 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ dom 𝐹((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
7155, 64, 703bitr2d 215 1 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − 𝐶)) < 𝑥))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1314  wcel 1463  wnfc 2243  wral 2391  wrex 2392  {crab 2395  Vcvv 2658  wss 3039   class class class wbr 3897  dom cdm 4507  wf 5087  cfv 5091  (class class class)co 5740  pm cpm 6509  cc 7582   < clt 7764  cmin 7897   # cap 8306  +crp 9393  abscabs 10720   lim climc 12698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-cnex 7675
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-rab 2400  df-v 2660  df-sbc 2881  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099  df-ov 5743  df-oprab 5744  df-mpo 5745  df-pm 6511  df-limced 12700
This theorem is referenced by:  ellimc3ap  12705  limcmpted  12707
  Copyright terms: Public domain W3C validator