![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lattrd | Structured version Visualization version GIF version |
Description: A lattice ordering is transitive. Deduction version of lattr 18443. (Contributed by NM, 3-Sep-2012.) |
Ref | Expression |
---|---|
lattrd.b | ⊢ 𝐵 = (Base‘𝐾) |
lattrd.l | ⊢ ≤ = (le‘𝐾) |
lattrd.1 | ⊢ (𝜑 → 𝐾 ∈ Lat) |
lattrd.2 | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
lattrd.3 | ⊢ (𝜑 → 𝑌 ∈ 𝐵) |
lattrd.4 | ⊢ (𝜑 → 𝑍 ∈ 𝐵) |
lattrd.5 | ⊢ (𝜑 → 𝑋 ≤ 𝑌) |
lattrd.6 | ⊢ (𝜑 → 𝑌 ≤ 𝑍) |
Ref | Expression |
---|---|
lattrd | ⊢ (𝜑 → 𝑋 ≤ 𝑍) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lattrd.5 | . 2 ⊢ (𝜑 → 𝑋 ≤ 𝑌) | |
2 | lattrd.6 | . 2 ⊢ (𝜑 → 𝑌 ≤ 𝑍) | |
3 | lattrd.1 | . . 3 ⊢ (𝜑 → 𝐾 ∈ Lat) | |
4 | lattrd.2 | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
5 | lattrd.3 | . . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐵) | |
6 | lattrd.4 | . . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐵) | |
7 | lattrd.b | . . . 4 ⊢ 𝐵 = (Base‘𝐾) | |
8 | lattrd.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
9 | 7, 8 | lattr 18443 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
10 | 3, 4, 5, 6, 9 | syl13anc 1369 | . 2 ⊢ (𝜑 → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
11 | 1, 2, 10 | mp2and 697 | 1 ⊢ (𝜑 → 𝑋 ≤ 𝑍) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 class class class wbr 5152 ‘cfv 6553 Basecbs 17187 lecple 17247 Latclat 18430 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-nul 5310 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-opab 5215 df-xp 5688 df-dm 5692 df-iota 6505 df-fv 6561 df-poset 18312 df-lat 18431 |
This theorem is referenced by: latmlej11 18477 latjass 18482 lubun 18514 cvlcvr1 38843 exatleN 38909 2atjm 38950 2llnmat 39029 llnmlplnN 39044 2llnjaN 39071 2lplnja 39124 dalem5 39172 lncmp 39288 2lnat 39289 2llnma1b 39291 cdlema1N 39296 paddasslem5 39329 paddasslem12 39336 paddasslem13 39337 dalawlem3 39378 dalawlem5 39380 dalawlem6 39381 dalawlem7 39382 dalawlem8 39383 dalawlem11 39386 dalawlem12 39387 pl42lem1N 39484 lhpexle2lem 39514 lhpexle3lem 39516 4atexlemtlw 39572 4atexlemc 39574 cdleme15 39783 cdleme17b 39792 cdleme22e 39849 cdleme22eALTN 39850 cdleme23a 39854 cdleme28a 39875 cdleme30a 39883 cdleme32e 39950 cdleme35b 39955 trlord 40074 cdlemg10 40146 cdlemg11b 40147 cdlemg17a 40166 cdlemg35 40218 tendococl 40277 tendopltp 40285 cdlemi1 40323 cdlemk11 40354 cdlemk5u 40366 cdlemk11u 40376 cdlemk52 40459 dialss 40551 diaglbN 40560 diaintclN 40563 dia2dimlem1 40569 cdlemm10N 40623 djajN 40642 dibglbN 40671 dibintclN 40672 diblss 40675 cdlemn10 40711 dihord1 40723 dihord2pre2 40731 dihopelvalcpre 40753 dihord5apre 40767 dihmeetlem1N 40795 dihglblem2N 40799 dihmeetlem2N 40804 dihglbcpreN 40805 dihmeetlem3N 40810 |
Copyright terms: Public domain | W3C validator |