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=\mathrm{ran}G$$
Assertion	grpocl	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\wedge B\in X\right)\to AGB\in X$$

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	$$⊢X=\mathrm{ran}G$$
2	1	grpofo	$$⊢G\in \mathrm{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 \mathrm{GrpOp}\to G:X\times X⟶X$$
5		fovrn	$$⊢\left(G:X\times X⟶X\wedge A\in X\wedge B\in X\right)\to AGB\in X$$
6	4 5	syl3an1	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\wedge B\in X\right)\to AGB\in X$$