plttr

Description: The less-than relation is transitive. ( psstr analog.) (Contributed by NM, 2-Dec-2011)

	Ref	Expression
Hypotheses	pltnlt.b	$⊢ B = {Base}_{K}$
	pltnlt.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		pltnlt.b	$⊢ B = {Base}_{K}$
2		pltnlt.s	$⊢ \underset{˙}{<} = <_{K}$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	3 2	pltle	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to X \leq_{K} Y)$
5	4	3adant3r3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{<} Y \to X \leq_{K} Y)$
6	3 2	pltle	$⊢ (K \in Poset \land Y \in B \land Z \in B) \to (Y \underset{˙}{<} Z \to Y \leq_{K} Z)$
7	6	3adant3r1	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{<} Z \to Y \leq_{K} Z)$
8	1 3	postr	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \leq_{K} Y \land Y \leq_{K} Z) \to X \leq_{K} Z)$
9	5 7 8	syl2and	$⊢ (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 \leq_{K} Z)$
10	1 2	pltn2lp	$⊢ (K \in Poset \land X \in B \land Y \in B) \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} X)$
11	10	3adant3r3	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} X)$
12		breq2	$⊢ X = Z \to (Y \underset{˙}{<} X \leftrightarrow Y \underset{˙}{<} Z)$
13	12	anbi2d	$⊢ X = Z \to ((X \underset{˙}{<} Y \land Y \underset{˙}{<} X) \leftrightarrow (X \underset{˙}{<} Y \land Y \underset{˙}{<} Z))$
14	13	notbid	$⊢ X = Z \to (\neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} X) \leftrightarrow \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} Z))$
15	11 14	syl5ibcom	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X = Z \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} Z))$
16	15	necon2ad	$⊢ (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 \neq Z)$
17	9 16	jcad	$⊢ (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 \leq_{K} Z \land X \neq Z))$
18	3 2	pltval	$⊢ (K \in Poset \land X \in B \land Z \in B) \to (X \underset{˙}{<} Z \leftrightarrow (X \leq_{K} Z \land X \neq Z))$
19	18	3adant3r2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{<} Z \leftrightarrow (X \leq_{K} Z \land X \neq Z))$
20	17 19	sylibrd	$⊢ (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)$

Metamath Proof Explorer

Theorem plttr

Proof