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	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	rngone0.2	⊢ 𝑋 = ran 𝐺
Assertion	rngone0	⊢ ( 𝑅 ∈ RingOps → 𝑋 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		rngone0.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		rngone0.2	⊢ 𝑋 = ran 𝐺
3	1	rngogrpo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
4	2	grpon0	⊢ ( 𝐺 ∈ GrpOp → 𝑋 ≠ ∅ )
5	3 4	syl	⊢ ( 𝑅 ∈ RingOps → 𝑋 ≠ ∅ )