Metamath Proof Explorer


Theorem lattr

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

Proof

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