![]() |
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 17537. (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 17537 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
10 | 3, 4, 5, 6, 9 | syl13anc 1353 | . 2 ⊢ (𝜑 → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
11 | 1, 2, 10 | mp2and 687 | 1 ⊢ (𝜑 → 𝑋 ≤ 𝑍) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1508 ∈ wcel 2051 class class class wbr 4926 ‘cfv 6186 Basecbs 16338 lecple 16427 Latclat 17526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2745 ax-nul 5064 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-xp 5410 df-dm 5414 df-iota 6150 df-fv 6194 df-poset 17427 df-lat 17527 |
This theorem is referenced by: latmlej11 17571 latjass 17576 lubun 17604 cvlcvr1 35953 exatleN 36018 2atjm 36059 2llnmat 36138 llnmlplnN 36153 2llnjaN 36180 2lplnja 36233 dalem5 36281 lncmp 36397 2lnat 36398 2llnma1b 36400 cdlema1N 36405 paddasslem5 36438 paddasslem12 36445 paddasslem13 36446 dalawlem3 36487 dalawlem5 36489 dalawlem6 36490 dalawlem7 36491 dalawlem8 36492 dalawlem11 36495 dalawlem12 36496 pl42lem1N 36593 lhpexle2lem 36623 lhpexle3lem 36625 4atexlemtlw 36681 4atexlemc 36683 cdleme15 36892 cdleme17b 36901 cdleme22e 36958 cdleme22eALTN 36959 cdleme23a 36963 cdleme28a 36984 cdleme30a 36992 cdleme32e 37059 cdleme35b 37064 trlord 37183 cdlemg10 37255 cdlemg11b 37256 cdlemg17a 37275 cdlemg35 37327 tendococl 37386 tendopltp 37394 cdlemi1 37432 cdlemk11 37463 cdlemk5u 37475 cdlemk11u 37485 cdlemk52 37568 dialss 37660 diaglbN 37669 diaintclN 37672 dia2dimlem1 37678 cdlemm10N 37732 djajN 37751 dibglbN 37780 dibintclN 37781 diblss 37784 cdlemn10 37820 dihord1 37832 dihord2pre2 37840 dihopelvalcpre 37862 dihord5apre 37876 dihmeetlem1N 37904 dihglblem2N 37908 dihmeetlem2N 37913 dihglbcpreN 37914 dihmeetlem3N 37919 |
Copyright terms: Public domain | W3C validator |