Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > latlem12 | Structured version Visualization version GIF version |
Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.) |
Ref | Expression |
---|---|
latmle.b | ⊢ 𝐵 = (Base‘𝐾) |
latmle.l | ⊢ ≤ = (le‘𝐾) |
latmle.m | ⊢ ∧ = (meet‘𝐾) |
Ref | Expression |
---|---|
latlem12 | ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latmle.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | latmle.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | latmle.m | . 2 ⊢ ∧ = (meet‘𝐾) | |
4 | latpos 17660 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
5 | 4 | adantr 483 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset) |
6 | simpr2 1191 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | |
7 | simpr3 1192 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | |
8 | simpr1 1190 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | |
9 | eqid 2821 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
10 | simpl 485 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat) | |
11 | 1, 9, 3, 10, 6, 7 | latcl2 17658 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (〈𝑌, 𝑍〉 ∈ dom (join‘𝐾) ∧ 〈𝑌, 𝑍〉 ∈ dom ∧ )) |
12 | 11 | simprd 498 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 〈𝑌, 𝑍〉 ∈ dom ∧ ) |
13 | 1, 2, 3, 5, 6, 7, 8, 12 | meetle 17638 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 〈cop 4573 class class class wbr 5066 dom cdm 5555 ‘cfv 6355 (class class class)co 7156 Basecbs 16483 lecple 16572 Posetcpo 17550 joincjn 17554 meetcmee 17555 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-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
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-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-poset 17556 df-glb 17585 df-meet 17587 df-lat 17656 |
This theorem is referenced by: latleeqm1 17689 latmlem1 17691 latmidm 17696 latledi 17699 mod1ile 17715 oldmm1 36368 olm01 36387 cmtbr4N 36406 atnle 36468 atlatmstc 36470 hlrelat2 36554 cvrval5 36566 cvrexchlem 36570 2atjm 36596 atbtwn 36597 ps-2b 36633 2atm 36678 2llnm4 36721 2llnmeqat 36722 dalemcea 36811 dalem21 36845 dalem54 36877 dalem55 36878 dalem57 36880 2atm2atN 36936 2llnma1b 36937 cdlemblem 36944 dalawlem2 37023 dalawlem3 37024 dalawlem6 37027 dalawlem11 37032 dalawlem12 37033 lhpocnle 37167 lhpmcvr4N 37177 lhpat3 37197 4atexlemcnd 37223 lautm 37245 trlval3 37338 cdlemc5 37346 cdleme3 37388 cdleme7ga 37399 cdleme7 37400 cdleme11k 37419 cdleme16e 37433 cdleme16f 37434 cdlemednpq 37450 cdleme22aa 37490 cdleme22b 37492 cdleme22cN 37493 cdleme23c 37502 cdlemeg46req 37680 cdlemf2 37713 cdlemg10c 37790 cdlemg12f 37799 cdlemg17dALTN 37815 cdlemg19a 37834 cdlemg27b 37847 cdlemi 37971 cdlemk15 38006 cdlemk50 38103 dia2dimlem1 38215 dihopelvalcpre 38399 dihord5b 38410 dihmeetlem1N 38441 dihglblem5apreN 38442 dihglblem2N 38445 dihmeetlem3N 38456 |
Copyright terms: Public domain | W3C validator |