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