![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > posref | Structured version Visualization version GIF version |
Description: A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Ref | Expression |
---|---|
posi.b | ⊢ 𝐵 = (Base‘𝐾) |
posi.l | ⊢ ≤ = (le‘𝐾) |
Ref | Expression |
---|---|
posref | ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | posprs 18311 | . 2 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset ) | |
2 | posi.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | posi.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
4 | 2, 3 | prsref 18294 | . 2 ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
5 | 1, 4 | sylan 578 | 1 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 class class class wbr 5149 ‘cfv 6549 Basecbs 17183 lecple 17243 Proset cproset 18288 Posetcpo 18302 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-nul 5307 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-proset 18290 df-poset 18308 |
This theorem is referenced by: posasymb 18314 odupos 18323 pleval2 18332 pltval3 18334 pospo 18340 lublecllem 18355 latref 18436 omndmul2 32882 omndmul 32884 gsumle 32894 archirngz 32989 cvrnbtwn2 38877 cvrnbtwn3 38878 cvrnbtwn4 38881 cvrcmp 38885 llncmp 39125 lplncmp 39165 lvolcmp 39220 lubprlem 48167 posjidm 48177 posmidm 48178 |
Copyright terms: Public domain | W3C validator |