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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	posi.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		posi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		posi.l	⊢ ≤ = ( le ‘ 𝐾 )
3		posprs	⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )
4	1 2	prsref	⊢ ( ( 𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
5	3 4	sylan	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )