Theorem grpofo

Description: A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	grpfo.1	⊢ 𝑋 = ran 𝐺
Assertion	grpofo	⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	⊢ 𝑋 = ran 𝐺
2	1	isgrpo	⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
3	2	ibi	⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
4	3	simp1d	⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
5	1	eqcomi	⊢ ran 𝐺 = 𝑋
6	4 5	jctir	⊢ ( 𝐺 ∈ GrpOp → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ran 𝐺 = 𝑋 ) )
7		dffo2	⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ran 𝐺 = 𝑋 ) )
8	6 7	sylibr	⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )