Definition df-ps

Description: Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008)

	Ref	Expression
Assertion	df-ps	⊢ PosetRel = { 𝑟 ∣ ( Rel 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cps	⊢ PosetRel
1		vr	⊢ 𝑟
2	1	cv	⊢ 𝑟
3	2	wrel	⊢ Rel 𝑟
4	2 2	ccom	⊢ ( 𝑟 ∘ 𝑟 )
5	4 2	wss	⊢ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟
6	2	ccnv	⊢ ◡ 𝑟
7	2 6	cin	⊢ ( 𝑟 ∩ ◡ 𝑟 )
8		cid	⊢ I
9	2	cuni	⊢ ∪ 𝑟
10	9	cuni	⊢ ∪ ∪ 𝑟
11	8 10	cres	⊢ ( I ↾ ∪ ∪ 𝑟 )
12	7 11	wceq	⊢ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 )
13	3 5 12	w3a	⊢ ( Rel 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) )
14	13 1	cab	⊢ { 𝑟 ∣ ( Rel 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) ) }
15	0 14	wceq	⊢ PosetRel = { 𝑟 ∣ ( Rel 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) ) }