This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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