Definition df-strict 5905

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 ∩ Connex )

Detailed syntax breakdown of Definition df-strict

Step	Hyp	Ref	Expression
1		cstrict 5894	. 2 class Or
2		cpartial 5892	. . 3 class Po
3		cconnex 5893	. . 3 class Connex
4	2, 3	cin 3209	. 2 class ( Po ∩ Connex )
5	1, 4	wceq 1642	1 wff Or = ( Po ∩ Connex )

This definition is referenced by:  strictex  5919  sopc  5935