Theorem posref

Description: A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Hypotheses	posi.b	|- B = ( Base ` K )
	posi.l	|- .<_ = ( le ` K )
Assertion	posref	|- ( ( K e. Poset /\ X e. B ) -> X .<_ X )

Proof

Step	Hyp	Ref	Expression
1		posi.b	|- B = ( Base ` K )
2		posi.l	|- .<_ = ( le ` K )
3		posprs	|- ( K e. Poset -> K e. Proset )
4	1 2	prsref	|- ( ( K e. Proset /\ X e. B ) -> X .<_ X )
5	3 4	sylan	|- ( ( K e. Poset /\ X e. B ) -> X .<_ X )