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

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 ⊢ 𝑋 = 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→ 𝑋 )