prsref

Description: "Less than or equal to" is reflexive 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	prsref	$⊢ (K \in Proset \land X \in B) \to X \underset{˙}{\leq} X$

Step	Hyp	Ref	Expression
1		isprs.b	$⊢ B = {Base}_{K}$
2		isprs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		id	$⊢ X \in B \to X \in B$
4	3 3 3	3jca	$⊢ X \in B \to (X \in B \land X \in B \land X \in B)$
5	1 2	prslem	$⊢ (K \in Proset \land (X \in B \land X \in B \land X \in B)) \to (X \underset{˙}{\leq} X \land ((X \underset{˙}{\leq} X \land X \underset{˙}{\leq} X) \to X \underset{˙}{\leq} X))$
6	4 5	sylan2	$⊢ (K \in Proset \land X \in B) \to (X \underset{˙}{\leq} X \land ((X \underset{˙}{\leq} X \land X \underset{˙}{\leq} X) \to X \underset{˙}{\leq} X))$
7	6	simpld	$⊢ (K \in Proset \land X \in B) \to X \underset{˙}{\leq} X$

Metamath Proof Explorer