Theorem qrngbas

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

	Ref	Expression
Hypothesis	qrng.q	|- Q = ( CCfld |`s QQ )
Assertion	qrngbas	|- QQ = ( Base ` Q )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	|- Q = ( CCfld |`s QQ )
2		qsscn	|- QQ C_ CC
3		cnfldbas	|- CC = ( Base ` CCfld )
4	1 3	ressbas2	|- ( QQ C_ CC -> QQ = ( Base ` Q ) )
5	2 4	ax-mp	|- QQ = ( Base ` Q )