Theorem plelttr

Description: Transitive law for chained "less than or equal to" and "less than". ( sspsstr analog.) (Contributed by NM, 2-May-2012)

	Ref	Expression
Hypotheses	pltletr.b	|- B = ( Base ` K )
	pltletr.l	|- .<_ = ( le ` K )
	pltletr.s	|- .< = ( lt ` K )
Assertion	plelttr	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .< Z ) -> X .< Z ) )

Proof

Step	Hyp	Ref	Expression
1		pltletr.b	|- B = ( Base ` K )
2		pltletr.l	|- .<_ = ( le ` K )
3		pltletr.s	|- .< = ( lt ` K )
4	1 2 3	pleval2	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) )
5	4	3adant3r3	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) )
6	1 3	plttr	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )
7	6	expd	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Y -> ( Y .< Z -> X .< Z ) ) )
8		breq1	|- ( X = Y -> ( X .< Z <-> Y .< Z ) )
9	8	biimprd	|- ( X = Y -> ( Y .< Z -> X .< Z ) )
10	9	a1i	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Y -> ( Y .< Z -> X .< Z ) ) )
11	7 10	jaod	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y \/ X = Y ) -> ( Y .< Z -> X .< Z ) ) )
12	5 11	sylbid	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( Y .< Z -> X .< Z ) ) )
13	12	impd	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .< Z ) -> X .< Z ) )