Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lattr | Structured version Visualization version GIF version |
Description: A lattice ordering is transitive. (sstr 3924 analog.) (Contributed by NM, 17-Nov-2011.) |
Ref | Expression |
---|---|
latref.b | ⊢ 𝐵 = (Base‘𝐾) |
latref.l | ⊢ ≤ = (le‘𝐾) |
Ref | Expression |
---|---|
lattr | ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latpos 17972 | . 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
2 | latref.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | latref.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
4 | 2, 3 | postr 17855 | . 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
5 | 1, 4 | sylan 583 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2111 class class class wbr 5068 ‘cfv 6398 Basecbs 16788 lecple 16837 Posetcpo 17842 Latclat 17965 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-nul 5214 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3423 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4253 df-if 4455 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4835 df-br 5069 df-opab 5131 df-xp 5572 df-dm 5576 df-iota 6356 df-fv 6406 df-poset 17848 df-lat 17966 |
This theorem is referenced by: lattrd 17980 latjlej1 17987 latjlej12 17989 latnlej2 17993 latmlem1 18003 latmlem12 18005 clatleglb 18052 lecmtN 37037 hlrelat2 37184 ps-2 37259 dalem3 37445 dalem17 37461 dalem21 37475 dalem25 37479 linepsubN 37533 pmapsub 37549 cdlemblem 37574 pmapjoin 37633 lhpmcvr4N 37807 4atexlemnclw 37851 cdlemd3 37981 cdleme3g 38015 cdleme3h 38016 cdleme7d 38027 cdleme21c 38108 cdleme32b 38223 cdleme35fnpq 38230 cdleme35f 38235 cdleme48bw 38283 cdlemf1 38342 cdlemg2fv2 38381 cdlemg7fvbwN 38388 cdlemg4 38398 cdlemg6c 38401 cdlemg27a 38473 cdlemg33b0 38482 cdlemg33a 38487 cdlemk3 38614 dia2dimlem1 38845 dihord6b 39041 dihord5apre 39043 dihglbcpreN 39081 |
Copyright terms: Public domain | W3C validator |