Metamath Proof Explorer

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

Proof

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 Y \in B \land Z \in B) \to (Y \underset{˙}{\leq} Z \leftrightarrow (Y \underset{˙}{<} Z \lor Y = Z))$
5	4	3adant3r1	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\leq} Z \leftrightarrow (Y \underset{˙}{<} Z \lor Y = Z))$
6	5	adantr	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{<} Y) \to (Y \underset{˙}{\leq} Z \leftrightarrow (Y \underset{˙}{<} Z \lor Y = Z))$
7	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)$
8	7	expdimp	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{<} Y) \to (Y \underset{˙}{<} Z \to X \underset{˙}{<} Z)$
9		breq2	$⊢ Y = Z \to (X \underset{˙}{<} Y \leftrightarrow X \underset{˙}{<} Z)$
10	9	biimpcd	$⊢ X \underset{˙}{<} Y \to (Y = Z \to X \underset{˙}{<} Z)$
11	10	adantl	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{<} Y) \to (Y = Z \to X \underset{˙}{<} Z)$
12	8 11	jaod	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{<} Y) \to ((Y \underset{˙}{<} Z \lor Y = Z) \to X \underset{˙}{<} Z)$
13	6 12	sylbid	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X \underset{˙}{<} Y) \to (Y \underset{˙}{\leq} Z \to X \underset{˙}{<} Z)$
14	13	expimpd	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{<} Z)$