![]() |
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 17264 | . 2 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset ) | |
2 | posi.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | posi.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
4 | 2, 3 | prsref 17247 | . 2 ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
5 | 1, 4 | sylan 576 | 1 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 class class class wbr 4843 ‘cfv 6101 Basecbs 16184 lecple 16274 Proset cproset 17241 Posetcpo 17255 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-nul 4983 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-iota 6064 df-fv 6109 df-proset 17243 df-poset 17261 |
This theorem is referenced by: posasymb 17267 pleval2 17280 pltval3 17282 pospo 17288 lublecllem 17303 latref 17368 odupos 17450 omndmul2 30228 omndmul 30230 archirngz 30259 gsumle 30295 cvrnbtwn2 35296 cvrnbtwn3 35297 cvrnbtwn4 35300 cvrcmp 35304 llncmp 35543 lplncmp 35583 lvolcmp 35638 |
Copyright terms: Public domain | W3C validator |