Theorem grpocl

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

	Ref	Expression
Hypothesis	grpfo.1	|- X = ran G
Assertion	grpocl	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G B ) e. X )

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	|- X = ran G
2	1	grpofo	|- ( G e. GrpOp -> G : ( X X. X ) -onto-> X )
3		fof	|- ( G : ( X X. X ) -onto-> X -> G : ( X X. X ) --> X )
4	2 3	syl	|- ( G e. GrpOp -> G : ( X X. X ) --> X )
5		fovcdm	|- ( ( G : ( X X. X ) --> X /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
6	4 5	syl3an1	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G B ) e. X )