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 𝐺