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 = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
	2zrngbas.r	|- R = ( CCfld |`s E )
Assertion	2zrngbas	|- E = ( Base ` R )

Proof

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