Theorem qrngbas

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

	Ref	Expression
Hypothesis	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
Assertion	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qsscn	$$⊢\mathbb{Q}\subseteq ℂ$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4	1 3	ressbas2	$$⊢\mathbb{Q}\subseteq ℂ\to \mathbb{Q}={\mathrm{Base}}_Q$$
5	2 4	ax-mp	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$