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	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		ssrab2	⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ⊆ ℤ
4		zsscn	⊢ ℤ ⊆ ℂ
5	3 4	sstri	⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ⊆ ℂ
6	1 5	eqsstri	⊢ 𝐸 ⊆ ℂ
7	2	cnfldsrngbas	⊢ ( 𝐸 ⊆ ℂ → 𝐸 = ( Base ‘ 𝑅 ) )
8	6 7	ax-mp	⊢ 𝐸 = ( Base ‘ 𝑅 )