![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > latref | Structured version Unicode version |
Description: A lattice ordering is reflexive. (ssid 3484 analog.) (Contributed by NM, 8-Oct-2011.) |
Ref | Expression |
---|---|
latref.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
latref.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
latref |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latpos 15340 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | latref.b |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | latref.l |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | posref 15241 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylan 471 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-nul 4530 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-rab 2808 df-v 3080 df-sbc 3295 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-br 4402 df-opab 4460 df-xp 4955 df-dm 4959 df-iota 5490 df-fv 5535 df-poset 15236 df-lat 15336 |
This theorem is referenced by: latleeqj1 15353 latjidm 15364 latleeqm1 15369 latmidm 15376 olj01 33209 olm01 33220 cmtidN 33241 ps-1 33460 3at 33473 llnneat 33497 2atnelpln 33527 lplnneat 33528 lplnnelln 33529 3atnelvolN 33569 lvolneatN 33571 lvolnelln 33572 lvolnelpln 33573 4at 33596 lplncvrlvol 33599 lncmp 33766 lhpocnle 33999 ltrnel 34122 ltrncnvel 34125 ltrnmw 34134 tendoidcl 34752 cdlemk39u 34951 dia1eldmN 35025 dia1N 35037 dihwN 35273 dihglblem5apreN 35275 dihmeetbclemN 35288 |
Copyright terms: Public domain | W3C validator |