Theorem qrngbas

Description: The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypothesis	qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion	qrngbas	⊢ ℚ = ( Base ‘ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qsscn	⊢ ℚ ⊆ ℂ
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4	1 3	ressbas2	⊢ ( ℚ ⊆ ℂ → ℚ = ( Base ‘ 𝑄 ) )
5	2 4	ax-mp	⊢ ℚ = ( Base ‘ 𝑄 )