Metamath Proof Explorer


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 ↾ 𝑟 ) ) }