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

Metamath Proof Explorer

Theorem idlimc

Description: Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses idlimc.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
idlimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
idlimc.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
Assertion idlimc ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 idlimc.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2 idlimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
3 idlimc.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
6 2 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
7 5 5 6 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
8 7 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) = ( abs ‘ ( 𝑥 − 𝑋 ) ) )
9 8 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) = ( abs ‘ ( 𝑥 − 𝑋 ) ) )
10 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 )
11 9 10 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 )
12 11 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 )
13 12 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) )
14 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) )
15 14 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) )
16 nfcv ⊢ Ⅎ 𝑧 𝑥
17 nfcv ⊢ Ⅎ 𝑧 𝑋
18 16 17 nfne ⊢ Ⅎ 𝑧 𝑥 ≠ 𝑋
19 nfv ⊢ Ⅎ 𝑧 ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤
20 18 19 nfan ⊢ Ⅎ 𝑧 ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 )
21 nfv ⊢ Ⅎ 𝑧 ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤
22 20 21 nfim ⊢ Ⅎ 𝑧 ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 )
23 nfv ⊢ Ⅎ 𝑥 ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 )
24 nfcv ⊢ Ⅎ 𝑥 abs
25 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
26 2 25 nfcxfr ⊢ Ⅎ 𝑥 𝐹
27 nfcv ⊢ Ⅎ 𝑥 𝑧
28 26 27 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
29 nfcv ⊢ Ⅎ 𝑥 −
30 nfcv ⊢ Ⅎ 𝑥 𝑋
31 28 29 30 nfov ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑧 ) − 𝑋 )
32 24 31 nffv ⊢ Ⅎ 𝑥 ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) )
33 nfcv ⊢ Ⅎ 𝑥 <
34 nfcv ⊢ Ⅎ 𝑥 𝑤
35 32 33 34 nfbr ⊢ Ⅎ 𝑥 ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤
36 23 35 nfim ⊢ Ⅎ 𝑥 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 )
37 neeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≠ 𝑋 ↔ 𝑧 ≠ 𝑋 ) )
38 fvoveq1 ⊢ ( 𝑥 = 𝑧 → ( abs ‘ ( 𝑥 − 𝑋 ) ) = ( abs ‘ ( 𝑧 − 𝑋 ) ) )
39 38 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ↔ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) )
40 37 39 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) ↔ ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) ) )
41 40 imbrov2fvoveq ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ↔ ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) )
42 22 36 41 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) )
43 15 42 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) )
44 brimralrspcev ⊢ ( ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) )
45 4 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) )
46 45 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) )
47 1 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
48 47 2 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
49 48 1 3 ellimc3 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 limℂ 𝑋 ) ↔ ( 𝑋 ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) ) )
50 3 46 49 mpbir2and ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝑋 ) )