Metamath Proof Explorer

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 ⊢ X = ran ⁡ G
Assertion grpofo ⊢ G ∈ GrpOp → G : X × X ⟶ onto X

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ X = ran ⁡ G
2 1 isgrpo ⊢ G ∈ GrpOp → G ∈ GrpOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
3 2 ibi ⊢ G ∈ GrpOp → G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
4 3 simp1d ⊢ G ∈ GrpOp → G : X × X ⟶ X
5 1 eqcomi ⊢ ran ⁡ G = X
6 4 5 jctir ⊢ G ∈ GrpOp → G : X × X ⟶ X ∧ ran ⁡ G = X
7 dffo2 ⊢ G : X × X ⟶ onto X ↔ G : X × X ⟶ X ∧ ran ⁡ G = X
8 6 7 sylibr ⊢ G ∈ GrpOp → G : X × X ⟶ onto X