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

Metamath Proof Explorer

Theorem grporn

Description: The range of a group operation. Useful for satisfying group base set hypotheses of the form X = ran G . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grprn.1 ⊢ 𝐺 ∈ GrpOp
grprn.2 ⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
Assertion grporn 𝑋 = ran 𝐺

Proof

Step Hyp Ref Expression
1 grprn.1 ⊢ 𝐺 ∈ GrpOp
2 grprn.2 ⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
3 eqid ⊢ ran 𝐺 = ran 𝐺
4 3 grpofo ⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 )
5 fofun ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → Fun 𝐺 )
6 1 4 5 mp2b ⊢ Fun 𝐺
7 df-fn ⊢ ( 𝐺 Fn ( 𝑋 × 𝑋 ) ↔ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝑋 × 𝑋 ) ) )
8 6 2 7 mpbir2an ⊢ 𝐺 Fn ( 𝑋 × 𝑋 )
9 fofn ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → 𝐺 Fn ( ran 𝐺 × ran 𝐺 ) )
10 1 4 9 mp2b ⊢ 𝐺 Fn ( ran 𝐺 × ran 𝐺 )
11 fndmu ⊢ ( ( 𝐺 Fn ( 𝑋 × 𝑋 ) ∧ 𝐺 Fn ( ran 𝐺 × ran 𝐺 ) ) → ( 𝑋 × 𝑋 ) = ( ran 𝐺 × ran 𝐺 ) )
12 xpid11 ⊢ ( ( 𝑋 × 𝑋 ) = ( ran 𝐺 × ran 𝐺 ) ↔ 𝑋 = ran 𝐺 )
13 11 12 sylib ⊢ ( ( 𝐺 Fn ( 𝑋 × 𝑋 ) ∧ 𝐺 Fn ( ran 𝐺 × ran 𝐺 ) ) → 𝑋 = ran 𝐺 )
14 8 10 13 mp2an ⊢ 𝑋 = ran 𝐺