Theorem 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={\mathrm{Base}}_K$$
	isprs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	prsref	$$⊢\left(K\in \mathrm{Proset}\wedge X\in B\right)\to X\underset{\dot{}}{\le }X$$

Proof

Step	Hyp	Ref	Expression
1		isprs.b	$$⊢B={\mathrm{Base}}_K$$
2		isprs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		id	$$⊢X\in B\to X\in B$$
4	3 3 3	3jca	$$⊢X\in B\to \left(X\in B\wedge X\in B\wedge X\in B\right)$$
5	1 2	prslem	$$⊢\left(K\in \mathrm{Proset}\wedge \left(X\in B\wedge X\in B\wedge X\in B\right)\right)\to \left(X\underset{\dot{}}{\le }X\wedge \left(\left(X\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\le }X\right)\to X\underset{\dot{}}{\le }X\right)\right)$$
6	4 5	sylan2	$$⊢\left(K\in \mathrm{Proset}\wedge X\in B\right)\to \left(X\underset{\dot{}}{\le }X\wedge \left(\left(X\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\le }X\right)\to X\underset{\dot{}}{\le }X\right)\right)$$
7	6	simpld	$$⊢\left(K\in \mathrm{Proset}\wedge X\in B\right)\to X\underset{\dot{}}{\le }X$$