Theorem oddibas

Description: Lemma 1 for oddinmgm : The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020)

	Ref	Expression
Hypotheses	oddinmgm.e	$$⊢O=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x+1\right\}$$
	oddinmgm.r	$$⊢M={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}O$$
Assertion	oddibas	$$⊢O={\mathrm{Base}}_M$$

Proof

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