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	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
	oddinmgm.r	⊢ 𝑀 = ( ℂfld ↾s 𝑂 )
Assertion	oddibas	⊢ 𝑂 = ( Base ‘ 𝑀 )

Proof

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