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 17056. (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 17056 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
10 | 3, 4, 5, 6, 9 | syl13anc 1328 | . 2 ⊢ (𝜑 → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) |
11 | 1, 2, 10 | mp2and 715 | 1 ⊢ (𝜑 → 𝑋 ≤ 𝑍) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 class class class wbr 4653 ‘cfv 5888 Basecbs 15857 lecple 15948 Latclat 17045 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-xp 5120 df-dm 5124 df-iota 5851 df-fv 5896 df-poset 16946 df-lat 17046 |
This theorem is referenced by: latmlej11 17090 latjass 17095 lubun 17123 cvlcvr1 34626 exatleN 34690 2atjm 34731 2llnmat 34810 llnmlplnN 34825 2llnjaN 34852 2lplnja 34905 dalem5 34953 lncmp 35069 2lnat 35070 2llnma1b 35072 cdlema1N 35077 paddasslem5 35110 paddasslem12 35117 paddasslem13 35118 dalawlem3 35159 dalawlem5 35161 dalawlem6 35162 dalawlem7 35163 dalawlem8 35164 dalawlem11 35167 dalawlem12 35168 pl42lem1N 35265 lhpexle2lem 35295 lhpexle3lem 35297 4atexlemtlw 35353 4atexlemc 35355 cdleme15 35565 cdleme17b 35574 cdleme22e 35632 cdleme22eALTN 35633 cdleme23a 35637 cdleme28a 35658 cdleme30a 35666 cdleme32e 35733 cdleme35b 35738 trlord 35857 cdlemg10 35929 cdlemg11b 35930 cdlemg17a 35949 cdlemg35 36001 tendococl 36060 tendopltp 36068 cdlemi1 36106 cdlemk11 36137 cdlemk5u 36149 cdlemk11u 36159 cdlemk52 36242 dialss 36335 diaglbN 36344 diaintclN 36347 dia2dimlem1 36353 cdlemm10N 36407 djajN 36426 dibglbN 36455 dibintclN 36456 diblss 36459 cdlemn10 36495 dihord1 36507 dihord2pre2 36515 dihopelvalcpre 36537 dihord5apre 36551 dihmeetlem1N 36579 dihglblem2N 36583 dihmeetlem2N 36588 dihglbcpreN 36589 dihmeetlem3N 36594 |
Copyright terms: Public domain | W3C validator |