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	|- .<_ = ( le ` K )
	lattrd.1	|- ( ph -> K e. Lat )
	lattrd.2	|- ( ph -> X e. B )
	lattrd.3	|- ( ph -> Y e. B )
	lattrd.4	|- ( ph -> Z e. B )
	lattrd.5	|- ( ph -> X .<_ Y )
	lattrd.6	|- ( ph -> Y .<_ Z )
Assertion	lattrd	|- ( ph -> X .<_ Z )

Proof

Step	Hyp	Ref	Expression
1		lattrd.b	|- B = ( Base ` K )
2		lattrd.l	|- .<_ = ( le ` K )
3		lattrd.1	|- ( ph -> K e. Lat )
4		lattrd.2	|- ( ph -> X e. B )
5		lattrd.3	|- ( ph -> Y e. B )
6		lattrd.4	|- ( ph -> Z e. B )
7		lattrd.5	|- ( ph -> X .<_ Y )
8		lattrd.6	|- ( ph -> Y .<_ Z )
9	1 2	lattr	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )
10	3 4 5 6 9	syl13anc	|- ( ph -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )
11	7 8 10	mp2and	|- ( ph -> X .<_ Z )