Definition df-strict 5904

Description: Define the set of all strict orderings over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-strict	|- Or = ( Po i^i Connex )

Detailed syntax breakdown of Definition df-strict

Step	Hyp	Ref	Expression
1		cstrict 5893	. 2 class Or
2		cpartial 5891	. . 3 class Po
3		cconnex 5892	. . 3 class Connex
4	2, 3	cin 3208	. 2 class ( Po i^i Connex )
5	1, 4	wceq 1642	1 wff Or = ( Po i^i Connex )

This definition is referenced by:  strictex  5918  sopc  5934