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 = ( 1st ` R )
rngone0.2 
|- X = ran G
Assertion rngone0 
|- ( R e. RingOps -> X =/= (/) )

Proof

Step Hyp Ref Expression
1 rngone0.1 
 |-  G = ( 1st ` R )
2 rngone0.2 
 |-  X = ran G
3 1 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
4 2 grpon0 
 |-  ( G e. GrpOp -> X =/= (/) )
5 3 4 syl 
 |-  ( R e. RingOps -> X =/= (/) )