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

Metamath Proof Explorer

Theorem grpon0

Description: The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 ⊢ 𝑋 = ran 𝐺
Assertion grpon0 ( 𝐺 ∈ GrpOp → 𝑋 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ 𝑋 = ran 𝐺
2 1 grpolidinv ⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
3 rexn0 ⊢ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) → 𝑋 ≠ ∅ )
4 2 3 syl ⊢ ( 𝐺 ∈ GrpOp → 𝑋 ≠ ∅ )