![]() |
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 3923 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 17652 | . 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
2 | latref.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
3 | latref.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
4 | 2, 3 | postr 17555 | . 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
5 | 1, 4 | sylan 583 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 class class class wbr 5030 ‘cfv 6324 Basecbs 16475 lecple 16564 Posetcpo 17542 Latclat 17647 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-nul 5174 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-xp 5525 df-dm 5529 df-iota 6283 df-fv 6332 df-poset 17548 df-lat 17648 |
This theorem is referenced by: lattrd 17660 latjlej1 17667 latjlej12 17669 latnlej2 17673 latmlem1 17683 latmlem12 17685 clatleglb 17728 lecmtN 36552 hlrelat2 36699 ps-2 36774 dalem3 36960 dalem17 36976 dalem21 36990 dalem25 36994 linepsubN 37048 pmapsub 37064 cdlemblem 37089 pmapjoin 37148 lhpmcvr4N 37322 4atexlemnclw 37366 cdlemd3 37496 cdleme3g 37530 cdleme3h 37531 cdleme7d 37542 cdleme21c 37623 cdleme32b 37738 cdleme35fnpq 37745 cdleme35f 37750 cdleme48bw 37798 cdlemf1 37857 cdlemg2fv2 37896 cdlemg7fvbwN 37903 cdlemg4 37913 cdlemg6c 37916 cdlemg27a 37988 cdlemg33b0 37997 cdlemg33a 38002 cdlemk3 38129 dia2dimlem1 38360 dihord6b 38556 dihord5apre 38558 dihglbcpreN 38596 |
Copyright terms: Public domain | W3C validator |