This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ogrp

Description: Define class of all ordered groups. An ordered group is a group with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 13-Mar-2018)

		Ref	Expression
	Assertion	df-ogrp	$⊢ oGrp = Grp \cap oMnd$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cogrp	$class oGrp$
1		cgrp	$class Grp$
2		comnd	$class oMnd$
3	1 2	cin	$class (Grp \cap oMnd)$
4	0 3	wceq	$wff oGrp = Grp \cap oMnd$