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 = ( Base ` K )
	isprs.l	|- .<_ = ( le ` K )
Assertion	prsref	|- ( ( K e. Proset /\ X e. B ) -> X .<_ X )

Proof

Step	Hyp	Ref	Expression
1		isprs.b	|- B = ( Base ` K )
2		isprs.l	|- .<_ = ( le ` K )
3		id	|- ( X e. B -> X e. B )
4	3 3 3	3jca	|- ( X e. B -> ( X e. B /\ X e. B /\ X e. B ) )
5	1 2	prslem	|- ( ( K e. Proset /\ ( X e. B /\ X e. B /\ X e. B ) ) -> ( X .<_ X /\ ( ( X .<_ X /\ X .<_ X ) -> X .<_ X ) ) )
6	4 5	sylan2	|- ( ( K e. Proset /\ X e. B ) -> ( X .<_ X /\ ( ( X .<_ X /\ X .<_ X ) -> X .<_ X ) ) )
7	6	simpld	|- ( ( K e. Proset /\ X e. B ) -> X .<_ X )