Theorem posref 18388

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

Hypotheses

Ref	Expression
posi.b	⊢ 𝐵 = (Base‘𝐾)
posi.l	⊢ ≤ = (le‘𝐾)

Assertion

Ref	Expression
posref	⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)

Proof of Theorem posref

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573  Basecbs 17258  lecple 17318   Proset cproset 18363  Posetcpo 18377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-proset 18365  df-poset 18383

This theorem is referenced by:  posasymb  18389  odupos  18398  pleval2  18407  pltval3  18409  pospo  18415  lublecllem  18430  latref  18511  omndmul2  33062  omndmul  33064  gsumle  33074  archirngz  33169  cvrnbtwn2  39231  cvrnbtwn3  39232  cvrnbtwn4  39235  cvrcmp  39239  llncmp  39479  lplncmp  39519  lvolcmp  39574  lubprlem  48642  posjidm  48652  posmidm  48653