Theorem rngone0

Description: The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngone0.1	$$⊢G=1^{st}\left(R\right)$$
	rngone0.2	$$⊢X=\mathrm{ran}G$$
Assertion	rngone0	$$⊢R\in \mathrm{RingOps}\to X\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rngone0.1	$$⊢G=1^{st}\left(R\right)$$
2		rngone0.2	$$⊢X=\mathrm{ran}G$$
3	1	rngogrpo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$
4	2	grpon0	$$⊢G\in \mathrm{GrpOp}\to X\ne \varnothing$$
5	3 4	syl	$$⊢R\in \mathrm{RingOps}\to X\ne \varnothing$$