postr

Description: A poset ordering is transitive. (Contributed by NM, 11-Sep-2011)

	Ref	Expression
Hypotheses	posi.b	$⊢ B = {Base}_{K}$
	posi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
Assertion	postr	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} Z)$

Step	Hyp	Ref	Expression
1		posi.b	$⊢ B = {Base}_{K}$
2		posi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3	1 2	posi	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} X \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y) \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} Z))$
4	3	simp3d	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} Z)$

Metamath Proof Explorer