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