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 = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
	oddinmgm.r	|- M = ( CCfld |`s O )
Assertion	oddibas	|- O = ( Base ` M )

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
2		oddinmgm.r	|- M = ( CCfld |`s O )
3		ssrab2	|- { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) } C_ ZZ
4	1 3	eqsstri	|- O C_ ZZ
5		zsscn	|- ZZ C_ CC
6	4 5	sstri	|- O C_ CC
7	2	cnfldsrngbas	|- ( O C_ CC -> O = ( Base ` M ) )
8	6 7	ax-mp	|- O = ( Base ` M )