Database
BASIC ORDER THEORY
Posets, directed sets, and lattices as relations
Posets and lattices as relations
df-ps
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 ↾ ∪ ∪ 𝑟 ) ) }