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 𝑋 ) )