climcncf

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	climcncf.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	climcncf.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climcncf.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
	climcncf.5	⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝐴 )
	climcncf.6	⊢ ( 𝜑 → 𝐺 ⇝ 𝐷 )
	climcncf.7	⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
Assertion	climcncf	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ⇝ ( 𝐹 ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		climcncf.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		climcncf.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climcncf.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
4		climcncf.5	⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝐴 )
5		climcncf.6	⊢ ( 𝜑 → 𝐺 ⇝ 𝐷 )
6		climcncf.7	⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
7		cncff	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
8	3 7	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9	8	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
10		cncfrss2	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐵 ⊆ ℂ )
11	3 10	syl	⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
12	11	sselda	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
13	9 12	syldan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
14	1	fvexi	⊢ 𝑍 ∈ V
15		fex	⊢ ( ( 𝐺 : 𝑍 ⟶ 𝐴 ∧ 𝑍 ∈ V ) → 𝐺 ∈ V )
16	4 14 15	sylancl	⊢ ( 𝜑 → 𝐺 ∈ V )
17		coexg	⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝐺 ∈ V ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
18	3 16 17	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ V )
19		cncfi	⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝐷 ∈ 𝐴 ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ 𝐴 ( ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐷 ) ) ) < 𝑥 ) )
20	19	3expia	⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( 𝑥 ∈ ℝ⁺ → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ 𝐴 ( ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐷 ) ) ) < 𝑥 ) ) )
21	3 6 20	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ 𝐴 ( ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐷 ) ) ) < 𝑥 ) ) )
22	21	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ ℝ⁺ ∀ 𝑧 ∈ 𝐴 ( ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐷 ) ) ) < 𝑥 ) )
23	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐴 )
24		fvco3	⊢ ( ( 𝐺 : 𝑍 ⟶ 𝐴 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
25	4 24	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
26	1 2 6 13 5 18 22 23 25	climcn1	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ⇝ ( 𝐹 ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem climcncf

Proof