| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | idlimc.x | . 2
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 2 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) | 
| 3 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | 
| 4 |  | idlimc.f | . . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥) | 
| 5 | 4 | fvmpt2 7027 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝑥) | 
| 6 | 3, 3, 5 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝑥) | 
| 7 | 6 | fvoveq1d 7453 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘(𝑥 − 𝑋))) | 
| 8 | 7 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘(𝑥 − 𝑋))) | 
| 9 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘(𝑥 − 𝑋)) < 𝑤) | 
| 10 | 8, 9 | eqbrtrd 5165 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) | 
| 11 | 10 | adantrl 716 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤)) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) | 
| 12 | 11 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) | 
| 13 | 12 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) | 
| 14 | 13 | ralrimiva 3146 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑥 ∈ 𝐴 ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) | 
| 15 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑧𝑥 | 
| 16 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑧𝑋 | 
| 17 | 15, 16 | nfne 3043 | . . . . . . . 8
⊢
Ⅎ𝑧 𝑥 ≠ 𝑋 | 
| 18 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑧(abs‘(𝑥 − 𝑋)) < 𝑤 | 
| 19 | 17, 18 | nfan 1899 | . . . . . . 7
⊢
Ⅎ𝑧(𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) | 
| 20 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑧(abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤 | 
| 21 | 19, 20 | nfim 1896 | . . . . . 6
⊢
Ⅎ𝑧((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) | 
| 22 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑥(𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) | 
| 23 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑥abs | 
| 24 |  | nfmpt1 5250 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝑥) | 
| 25 | 4, 24 | nfcxfr 2903 | . . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 | 
| 26 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑥𝑧 | 
| 27 | 25, 26 | nffv 6916 | . . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑧) | 
| 28 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑥
− | 
| 29 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑋 | 
| 30 | 27, 28, 29 | nfov 7461 | . . . . . . . . 9
⊢
Ⅎ𝑥((𝐹‘𝑧) − 𝑋) | 
| 31 | 23, 30 | nffv 6916 | . . . . . . . 8
⊢
Ⅎ𝑥(abs‘((𝐹‘𝑧) − 𝑋)) | 
| 32 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑥
< | 
| 33 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑥𝑤 | 
| 34 | 31, 32, 33 | nfbr 5190 | . . . . . . 7
⊢
Ⅎ𝑥(abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤 | 
| 35 | 22, 34 | nfim 1896 | . . . . . 6
⊢
Ⅎ𝑥((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) | 
| 36 |  | neeq1 3003 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ≠ 𝑋 ↔ 𝑧 ≠ 𝑋)) | 
| 37 |  | fvoveq1 7454 | . . . . . . . . 9
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 − 𝑋)) = (abs‘(𝑧 − 𝑋))) | 
| 38 | 37 | breq1d 5153 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → ((abs‘(𝑥 − 𝑋)) < 𝑤 ↔ (abs‘(𝑧 − 𝑋)) < 𝑤)) | 
| 39 | 36, 38 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) ↔ (𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤))) | 
| 40 | 39 | imbrov2fvoveq 7456 | . . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) ↔ ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) | 
| 41 | 21, 35, 40 | cbvralw 3306 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) | 
| 42 | 14, 41 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) | 
| 43 |  | brimralrspcev 5204 | . . . 4
⊢ ((𝑤 ∈ ℝ+
∧ ∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) | 
| 44 | 2, 42, 43 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) | 
| 45 | 44 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) | 
| 46 |  | idlimc.a | . . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 47 | 46 | sselda 3983 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) | 
| 48 | 47, 4 | fmptd 7134 | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 49 | 48, 46, 1 | ellimc3 25914 | . 2
⊢ (𝜑 → (𝑋 ∈ (𝐹 limℂ 𝑋) ↔ (𝑋 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)))) | 
| 50 | 1, 45, 49 | mpbir2and 713 | 1
⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋)) |