Description: A lattice ordering is transitive. ( sstr analog.) (Contributed by NM, 17-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | latref.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
latref.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
Assertion | lattr | ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latref.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
2 | latref.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
3 | latpos | ⊢ ( 𝐾 ∈ Lat → 𝐾 ∈ Poset ) | |
4 | 1 2 | postr | ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) |
5 | 3 4 | sylan | ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) |