Theorem prstr

Description: "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		isprs.b	|- B = ( Base ` K )
2		isprs.l	|- .<_ = ( le ` K )
3	1 2	prslem	|- ( ( K e. Proset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )
4	3	simprd	|- ( ( K e. Proset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )
5	4	3impia	|- ( ( K e. Proset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> X .<_ Z )