Theorem rlimcn1 14167

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.)

Hypotheses

Ref	Expression
rlimcn1.1	⊢ (𝜑 → 𝐺:𝐴⟶𝑋)
rlimcn1.2	⊢ (𝜑 → 𝐶 ∈ 𝑋)
rlimcn1.3	⊢ (𝜑 → 𝐺 ⇝𝑟 𝐶)
rlimcn1.4	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
rlimcn1.5	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))

Assertion

Ref	Expression
rlimcn1	⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝𝑟 (𝐹‘𝐶))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝑧,𝐹,𝑦   𝑥,𝐺,𝑦,𝑧   𝜑,𝑥,𝑦   𝑥,𝐶,𝑦,𝑧   𝑧,𝑋

Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑧)   𝑋(𝑥,𝑦)

Proof of Theorem rlimcn1

Dummy variables 𝑤 𝑐 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rlimcn1.1	. . . 4 ⊢ (𝜑 → 𝐺:𝐴⟶𝑋)
2	1	ffvelrnda 6267	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ 𝑋)
3	1	feqmptd 6159	. . 3 ⊢ (𝜑 → 𝐺 = (𝑤 ∈ 𝐴 ↦ (𝐺‘𝑤)))
4		rlimcn1.4	. . . 4 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
5	4	feqmptd 6159	. . 3 ⊢ (𝜑 → 𝐹 = (𝑣 ∈ 𝑋 ↦ (𝐹‘𝑣)))
6		fveq2 6103	. . 3 ⊢ (𝑣 = (𝐺‘𝑤) → (𝐹‘𝑣) = (𝐹‘(𝐺‘𝑤)))
7	2, 3, 5, 6	fmptco 6303	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐺) = (𝑤 ∈ 𝐴 ↦ (𝐹‘(𝐺‘𝑤))))
8		rlimcn1.5	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))
9		fvex 6113	. . . . . . . . . 10 ⊢ (𝐺‘𝑤) ∈ V
10	9	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ V)
11	10	ralrimiva 2949	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → ∀𝑤 ∈ 𝐴 (𝐺‘𝑤) ∈ V)
12		simpr 476	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
13		rlimcn1.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⇝𝑟 𝐶)
14	3, 13	eqbrtrrd 4607	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (𝐺‘𝑤)) ⇝𝑟 𝐶)
15	14	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → (𝑤 ∈ 𝐴 ↦ (𝐺‘𝑤)) ⇝𝑟 𝐶)
16	11, 12, 15	rlimi 14092	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦))
17		simpll 786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) → 𝜑)
18	17, 2	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ 𝑋)
19		simplrr 797	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) ∧ 𝑤 ∈ 𝐴) → ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))
20		oveq1 6556	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐺‘𝑤) → (𝑧 − 𝐶) = ((𝐺‘𝑤) − 𝐶))
21	20	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐺‘𝑤) → (abs‘(𝑧 − 𝐶)) = (abs‘((𝐺‘𝑤) − 𝐶)))
22	21	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘𝑤) → ((abs‘(𝑧 − 𝐶)) < 𝑦 ↔ (abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦))
23		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝐺‘𝑤) → (𝐹‘𝑧) = (𝐹‘(𝐺‘𝑤)))
24	23	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝐺‘𝑤) → ((𝐹‘𝑧) − (𝐹‘𝐶)) = ((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶)))
25	24	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐺‘𝑤) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) = (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))))
26	25	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐺‘𝑤) → ((abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥 ↔ (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥))
27	22, 26	imbi12d 333	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐺‘𝑤) → (((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥) ↔ ((abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
28	27	rspcv 3278	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑤) ∈ 𝑋 → (∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥) → ((abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
29	18, 19, 28	sylc 63	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) ∧ 𝑤 ∈ 𝐴) → ((abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥))
30	29	imim2d 55	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) ∧ 𝑤 ∈ 𝐴) → ((𝑐 ≤ 𝑤 → (abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦) → (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
31	30	ralimdva 2945	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) → (∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦) → ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
32	31	reximdv 2999	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥))) → (∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦) → ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
33	32	expr 641	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → (∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥) → (∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐺‘𝑤) − 𝐶)) < 𝑦) → ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥))))
34	16, 33	mpid 43	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+) → (∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
35	34	rexlimdva 3013	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝑋 ((abs‘(𝑧 − 𝐶)) < 𝑦 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐶))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
36	8, 35	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥))
37	36	ralrimiva 2949	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥))
38	4	ffvelrnda 6267	. . . . . 6 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ 𝑋) → (𝐹‘(𝐺‘𝑤)) ∈ ℂ)
39	2, 38	syldan 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘(𝐺‘𝑤)) ∈ ℂ)
40	39	ralrimiva 2949	. . . 4 ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 (𝐹‘(𝐺‘𝑤)) ∈ ℂ)
41		fdm 5964	. . . . . 6 ⊢ (𝐺:𝐴⟶𝑋 → dom 𝐺 = 𝐴)
42	1, 41	syl 17	. . . . 5 ⊢ (𝜑 → dom 𝐺 = 𝐴)
43		rlimss 14081	. . . . . 6 ⊢ (𝐺 ⇝𝑟 𝐶 → dom 𝐺 ⊆ ℝ)
44	13, 43	syl 17	. . . . 5 ⊢ (𝜑 → dom 𝐺 ⊆ ℝ)
45	42, 44	eqsstr3d 3603	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
46		rlimcn1.2	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
47	4, 46	ffvelrnd 6268	. . . 4 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
48	40, 45, 47	rlim2 14075	. . 3 ⊢ (𝜑 → ((𝑤 ∈ 𝐴 ↦ (𝐹‘(𝐺‘𝑤))) ⇝𝑟 (𝐹‘𝐶) ↔ ∀𝑥 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑐 ≤ 𝑤 → (abs‘((𝐹‘(𝐺‘𝑤)) − (𝐹‘𝐶))) < 𝑥)))
49	37, 48	mpbird 246	. 2 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (𝐹‘(𝐺‘𝑤))) ⇝𝑟 (𝐹‘𝐶))
50	7, 49	eqbrtrd 4605	1 ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝𝑟 (𝐹‘𝐶))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814   < clt 9953   ≤ cle 9954   − cmin 10145  ℝ⁺crp 11708  abscabs 13822   ⇝_𝑟 crli 14064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-pm 7747  df-rlim 14068

This theorem is referenced by:  rlimcn1b  14168  rlimdiv  14224