Metamath Proof Explorer


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 ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑌𝑌 𝑍 ) ) → 𝑋 𝑍 )