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 ⊢ 𝐺 = ( 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 → 𝑋 ≠ ∅ )