Metamath Proof Explorer

Theorem lattrd

Description: A lattice ordering is transitive. Deduction version of lattr . (Contributed by NM, 3-Sep-2012)

Ref Expression
Hypotheses lattrd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lattrd.l ⊢ ≤ = ( le ‘ 𝐾 )
lattrd.1 ⊢ ( 𝜑 → 𝐾 ∈ Lat )
lattrd.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
lattrd.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
lattrd.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
lattrd.5 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
lattrd.6 ⊢ ( 𝜑 → 𝑌 ≤ 𝑍 )
Assertion lattrd ( 𝜑 → 𝑋 ≤ 𝑍 )

Proof

Step Hyp Ref Expression
1 lattrd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lattrd.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lattrd.1 ⊢ ( 𝜑 → 𝐾 ∈ Lat )
4 lattrd.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 lattrd.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 lattrd.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7 lattrd.5 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
8 lattrd.6 ⊢ ( 𝜑 → 𝑌 ≤ 𝑍 )
9 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )
10 3 4 5 6 9 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )
11 7 8 10 mp2and ⊢ ( 𝜑 → 𝑋 ≤ 𝑍 )