![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latref | Structured version Visualization version GIF version |
Description: A lattice ordering is reflexive. (ssid 3969 analog.) (Contributed by NM, 8-Oct-2011.) |
Ref | Expression |
---|---|
latref.b | ⊢ 𝐵 = (Base‘𝐾) |
latref.l | ⊢ ≤ = (le‘𝐾) |
Ref | Expression |
---|---|
latref | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latpos 18341 | . 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
2 | latref.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | latref.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
4 | 2, 3 | posref 18221 | . 2 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
5 | 1, 4 | sylan 580 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 class class class wbr 5110 ‘cfv 6501 Basecbs 17094 lecple 17154 Posetcpo 18210 Latclat 18334 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-nul 5268 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rab 3406 df-v 3448 df-sbc 3743 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-xp 5644 df-dm 5648 df-iota 6453 df-fv 6509 df-proset 18198 df-poset 18216 df-lat 18335 |
This theorem is referenced by: latleeqj1 18354 latjidm 18365 latleeqm1 18370 latmidm 18377 olj01 37760 olm01 37771 cmtidN 37792 ps-1 38013 3at 38026 llnneat 38050 2atnelpln 38080 lplnneat 38081 lplnnelln 38082 3atnelvolN 38122 lvolneatN 38124 lvolnelln 38125 lvolnelpln 38126 4at 38149 lplncvrlvol 38152 lncmp 38319 lhpocnle 38552 ltrnel 38675 ltrncnvel 38678 tendoidcl 39305 cdlemk39u 39504 dia1eldmN 39577 dia1N 39589 dihwN 39825 dihglblem5apreN 39827 dihmeetbclemN 39840 |
Copyright terms: Public domain | W3C validator |