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

Metamath Proof Explorer

Theorem grporndm

Description: A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Assertion grporndm ( 𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran 𝐺 = ran 𝐺
2 1 grpofo ⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 )
3 fof ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 )
4 3 fdmd ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) )
5 4 dmeqd ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → dom dom 𝐺 = dom ( ran 𝐺 × ran 𝐺 ) )
6 dmxpid ⊢ dom ( ran 𝐺 × ran 𝐺 ) = ran 𝐺
7 5 6 eqtr2di ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → ran 𝐺 = dom dom 𝐺 )
8 2 7 syl ⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺 )