Theorem grpocl

Description: Closure law for a group operation. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	grpfo.1	⊢ 𝑋 = ran 𝐺
Assertion	grpocl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	⊢ 𝑋 = ran 𝐺
2	1	grpofo	⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )
3		fof	⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
4	2 3	syl	⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
5		fovcdm	⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
6	4 5	syl3an1	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )