Metamath Proof Explorer

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 \in GrpOp \land A \in X \land B \in X) \to A G B \in X$

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2	1	grpofo	$⊢ G \in GrpOp \to G : X \times X \underset{onto}{⟶} X$
3		fof	$⊢ G : X \times X \underset{onto}{⟶} X \to G : X \times X ⟶ X$
4	2 3	syl	$⊢ G \in GrpOp \to G : X \times X ⟶ X$
5		fovcdm	$⊢ (G : X \times X ⟶ X \land A \in X \land B \in X) \to A G B \in X$
6	4 5	syl3an1	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G B \in X$