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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isprs.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	prstr	⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝑋 ≤ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		isprs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isprs.l	⊢ ≤ = ( le ‘ 𝐾 )
3	1 2	prslem	⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )
4	3	simprd	⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )
5	4	3impia	⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝑋 ≤ 𝑍 )