prstr

Description: "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015)

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

Step	Hyp	Ref	Expression
1		isprs.b	$⊢ B = {Base}_{K}$
2		isprs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3	1 2	prslem	$⊢ (K \in Proset \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} Z) \to X \underset{˙}{\leq} Z))$
4	3	simprd	$⊢ (K \in Proset \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)$
5	4	3impia	$⊢ (K \in Proset \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Z)) \to X \underset{˙}{\leq} Z$

Metamath Proof Explorer