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 → 𝑋 ≠ ∅ )