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 B = Base K
lattrd.l ˙ = K
lattrd.1 φ K Lat
lattrd.2 φ X B
lattrd.3 φ Y B
lattrd.4 φ Z B
lattrd.5 φ X ˙ Y
lattrd.6 φ Y ˙ Z
Assertion lattrd φ X ˙ Z

Proof

Step Hyp Ref Expression
1 lattrd.b B = Base K
2 lattrd.l ˙ = K
3 lattrd.1 φ K Lat
4 lattrd.2 φ X B
5 lattrd.3 φ Y B
6 lattrd.4 φ Z B
7 lattrd.5 φ X ˙ Y
8 lattrd.6 φ Y ˙ Z
9 1 2 lattr K Lat X B Y B Z B X ˙ Y Y ˙ Z X ˙ Z
10 3 4 5 6 9 syl13anc φ X ˙ Y Y ˙ Z X ˙ Z
11 7 8 10 mp2and φ X ˙ Z