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 17666. (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 17666 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
10 | 3, 4, 5, 6, 9 | syl13anc 1368 | . 2 ⊢ (𝜑 → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
11 | 1, 2, 10 | mp2and 697 | 1 ⊢ (𝜑 → 𝑋 ≤ 𝑍) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 class class class wbr 5066 ‘cfv 6355 Basecbs 16483 lecple 16572 Latclat 17655 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-nul 5210 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-xp 5561 df-dm 5565 df-iota 6314 df-fv 6363 df-poset 17556 df-lat 17656 |
This theorem is referenced by: latmlej11 17700 latjass 17705 lubun 17733 cvlcvr1 36490 exatleN 36555 2atjm 36596 2llnmat 36675 llnmlplnN 36690 2llnjaN 36717 2lplnja 36770 dalem5 36818 lncmp 36934 2lnat 36935 2llnma1b 36937 cdlema1N 36942 paddasslem5 36975 paddasslem12 36982 paddasslem13 36983 dalawlem3 37024 dalawlem5 37026 dalawlem6 37027 dalawlem7 37028 dalawlem8 37029 dalawlem11 37032 dalawlem12 37033 pl42lem1N 37130 lhpexle2lem 37160 lhpexle3lem 37162 4atexlemtlw 37218 4atexlemc 37220 cdleme15 37429 cdleme17b 37438 cdleme22e 37495 cdleme22eALTN 37496 cdleme23a 37500 cdleme28a 37521 cdleme30a 37529 cdleme32e 37596 cdleme35b 37601 trlord 37720 cdlemg10 37792 cdlemg11b 37793 cdlemg17a 37812 cdlemg35 37864 tendococl 37923 tendopltp 37931 cdlemi1 37969 cdlemk11 38000 cdlemk5u 38012 cdlemk11u 38022 cdlemk52 38105 dialss 38197 diaglbN 38206 diaintclN 38209 dia2dimlem1 38215 cdlemm10N 38269 djajN 38288 dibglbN 38317 dibintclN 38318 diblss 38321 cdlemn10 38357 dihord1 38369 dihord2pre2 38377 dihopelvalcpre 38399 dihord5apre 38413 dihmeetlem1N 38441 dihglblem2N 38445 dihmeetlem2N 38450 dihglbcpreN 38451 dihmeetlem3N 38456 |
Copyright terms: Public domain | W3C validator |