Theorem 2zrngbas

Description: The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020)

	Ref	Expression
Hypotheses	2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
	2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
Assertion	2zrngbas	$$⊢E={\mathrm{Base}}_R$$

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
2		2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
3		ssrab2	$$⊢\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\subseteq \mathbb{Z}$$
4		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
5	3 4	sstri	$$⊢\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\subseteq ℂ$$
6	1 5	eqsstri	$$⊢E\subseteq ℂ$$
7	2	cnfldsrngbas	$$⊢E\subseteq ℂ\to E={\mathrm{Base}}_R$$
8	6 7	ax-mp	$$⊢E={\mathrm{Base}}_R$$