![]() |
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 3964 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 18319 | . 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
2 | latref.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | latref.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
4 | 2, 3 | posref 18199 | . 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 5103 ‘cfv 6493 Basecbs 17075 lecple 17132 Posetcpo 18188 Latclat 18312 |
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 2707 ax-nul 5261 |
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 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-ral 3063 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-xp 5637 df-dm 5641 df-iota 6445 df-fv 6501 df-proset 18176 df-poset 18194 df-lat 18313 |
This theorem is referenced by: latleeqj1 18332 latjidm 18343 latleeqm1 18348 latmidm 18355 olj01 37654 olm01 37665 cmtidN 37686 ps-1 37907 3at 37920 llnneat 37944 2atnelpln 37974 lplnneat 37975 lplnnelln 37976 3atnelvolN 38016 lvolneatN 38018 lvolnelln 38019 lvolnelpln 38020 4at 38043 lplncvrlvol 38046 lncmp 38213 lhpocnle 38446 ltrnel 38569 ltrncnvel 38572 tendoidcl 39199 cdlemk39u 39398 dia1eldmN 39471 dia1N 39483 dihwN 39719 dihglblem5apreN 39721 dihmeetbclemN 39734 |
Copyright terms: Public domain | W3C validator |