This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )