Theorem postr

Description: A poset ordering is transitive. (Contributed by NM, 11-Sep-2011)

	Ref	Expression
Hypotheses	posi.b	|- B = ( Base ` K )
	posi.l	|- .<_ = ( le ` K )
Assertion	postr	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )

Proof

Step	Hyp	Ref	Expression
1		posi.b	|- B = ( Base ` K )
2		posi.l	|- .<_ = ( le ` K )
3	1 2	posi	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )
4	3	simp3d	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )