This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⁡ R
rngone0.2 ⊢ X = ran ⁡ G
Assertion rngone0 ⊢ R ∈ RingOps → X ≠ ∅

Proof

Step Hyp Ref Expression
1 rngone0.1 ⊢ G = 1 st ⁡ R
2 rngone0.2 ⊢ X = ran ⁡ G
3 1 rngogrpo ⊢ R ∈ RingOps → G ∈ GrpOp
4 2 grpon0 ⊢ G ∈ GrpOp → X ≠ ∅
5 3 4 syl ⊢ R ∈ RingOps → X ≠ ∅