Theorem pltletr

Description: Transitive law for chained "less than" and "less than or equal to". ( psssstr analog.) (Contributed by NM, 2-Dec-2011)

	Ref	Expression
Hypotheses	pltletr.b	|- B = ( Base ` K )
	pltletr.l	|- .<_ = ( le ` K )
	pltletr.s	|- .< = ( lt ` K )
Assertion	pltletr	|- ( ( 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 /\ Y e. B /\ Z e. B ) -> ( Y .<_ Z <-> ( Y .< Z \/ Y = Z ) ) )
5	4	3adant3r1	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .<_ Z <-> ( Y .< Z \/ Y = Z ) ) )
6	5	adantr	|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y .<_ Z <-> ( Y .< Z \/ Y = Z ) ) )
7	1 3	plttr	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )
8	7	expdimp	|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y .< Z -> X .< Z ) )
9		breq2	|- ( Y = Z -> ( X .< Y <-> X .< Z ) )
10	9	biimpcd	|- ( X .< Y -> ( Y = Z -> X .< Z ) )
11	10	adantl	|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y = Z -> X .< Z ) )
12	8 11	jaod	|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( ( Y .< Z \/ Y = Z ) -> X .< Z ) )
13	6 12	sylbid	|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y .<_ Z -> X .< Z ) )
14	13	expimpd	|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .<_ Z ) -> X .< Z ) )