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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pltletr.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	plelttr	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{<} Z) \to X \underset{˙}{<} Z)$

Step	Hyp	Ref	Expression
1		pltletr.b	$⊢ B = {Base}_{K}$
2		pltletr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pltletr.s	$⊢ \underset{˙}{<} = <_{K}$
4	1 2 3	pleval2	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{<} Y \lor X = Y))$
5	4	3adant3r3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{<} Y \lor X = Y))$
6	1 3	plttr	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{<} Z) \to X \underset{˙}{<} Z)$
7	6	expd	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{<} Y \to (Y \underset{˙}{<} Z \to X \underset{˙}{<} Z))$
8		breq1	$⊢ X = Y \to (X \underset{˙}{<} Z \leftrightarrow Y \underset{˙}{<} Z)$
9	8	biimprd	$⊢ X = Y \to (Y \underset{˙}{<} Z \to X \underset{˙}{<} Z)$
10	9	a1i	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X = Y \to (Y \underset{˙}{<} Z \to X \underset{˙}{<} Z))$
11	7 10	jaod	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \lor X = Y) \to (Y \underset{˙}{<} Z \to X \underset{˙}{<} Z))$
12	5 11	sylbid	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Y \to (Y \underset{˙}{<} Z \to X \underset{˙}{<} Z))$
13	12	impd	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{<} Z) \to X \underset{˙}{<} Z)$

Metamath Proof Explorer