Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lattr | Structured version Visualization version Unicode version |
Description: A lattice ordering is transitive. (sstr 3611 analog.) (Contributed by NM, 17-Nov-2011.) |
Ref | Expression |
---|---|
latref.b | |
latref.l |
Ref | Expression |
---|---|
lattr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latpos 17050 | . 2 | |
2 | latref.b | . . 3 | |
3 | latref.l | . . 3 | |
4 | 2, 3 | postr 16953 | . 2 |
5 | 1, 4 | sylan 488 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 wceq 1483 wcel 1990 class class class wbr 4653 cfv 5888 cbs 15857 cple 15948 cpo 16940 clat 17045 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-xp 5120 df-dm 5124 df-iota 5851 df-fv 5896 df-poset 16946 df-lat 17046 |
This theorem is referenced by: lattrd 17058 latjlej1 17065 latjlej12 17067 latnlej2 17071 latmlem1 17081 latmlem12 17083 clatleglb 17126 lecmtN 34543 hlrelat2 34689 ps-2 34764 dalem3 34950 dalem17 34966 dalem21 34980 dalem25 34984 linepsubN 35038 pmapsub 35054 cdlemblem 35079 pmapjoin 35138 lhpmcvr4N 35312 4atexlemnclw 35356 cdlemd3 35487 cdleme3g 35521 cdleme3h 35522 cdleme7d 35533 cdleme21c 35615 cdleme32b 35730 cdleme35fnpq 35737 cdleme35f 35742 cdleme48bw 35790 cdlemf1 35849 cdlemg2fv2 35888 cdlemg7fvbwN 35895 cdlemg4 35905 cdlemg6c 35908 cdlemg27a 35980 cdlemg33b0 35989 cdlemg33a 35994 cdlemk3 36121 dia2dimlem1 36353 dihord6b 36549 dihord5apre 36551 dihglbcpreN 36589 |
Copyright terms: Public domain | W3C validator |