Theorem climconstmpt

Description: A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	climconstmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climconstmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climconstmpt.a	$$⊢\phi \to A\in ℂ$$
Assertion	climconstmpt	$$⊢\phi \to \left(x\in Z⟼A\right)⇝A$$

Proof

Step	Hyp	Ref	Expression
1		climconstmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		climconstmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		climconstmpt.a	$$⊢\phi \to A\in ℂ$$
4		fconstmpt	$$⊢Z\times \left\{A\right\}=\left(x\in Z⟼A\right)$$
5	2	eqcomi	$$⊢{\mathbb{Z}}_{\ge M}=Z$$
6		ssid	$$⊢Z\subseteq Z$$
7	5 6	eqsstri	$$⊢{\mathbb{Z}}_{\ge M}\subseteq Z$$
8	2	fvexi	$$⊢Z\in \mathrm{V}$$
9	7 8	climconst2	$$⊢\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\to \left(Z\times \left\{A\right\}\right)⇝A$$
10	3 1 9	syl2anc	$$⊢\phi \to \left(Z\times \left\{A\right\}\right)⇝A$$
11	4 10	eqbrtrrid	$$⊢\phi \to \left(x\in Z⟼A\right)⇝A$$