Theorem pstr2

Description: A poset is transitive. (Contributed by FL, 3-Aug-2009)

	Ref	Expression
Assertion	pstr2	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		isps	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∈ PosetRel ↔ ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) ) )
2	1	ibi	⊢ ( 𝑅 ∈ PosetRel → ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) )
3	2	simp2d	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )