Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > latmle2 | Structured version Visualization version GIF version |
Description: A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
Ref | Expression |
---|---|
latmle.b | ⊢ 𝐵 = (Base‘𝐾) |
latmle.l | ⊢ ≤ = (le‘𝐾) |
latmle.m | ⊢ ∧ = (meet‘𝐾) |
Ref | Expression |
---|---|
latmle2 | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latmle.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | latmle.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | latmle.m | . 2 ⊢ ∧ = (meet‘𝐾) | |
4 | simp1 1128 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
5 | simp2 1129 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
6 | simp3 1130 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
7 | eqid 2818 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
8 | 1, 7, 3, 4, 5, 6 | latcl2 17646 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom (join‘𝐾) ∧ 〈𝑋, 𝑌〉 ∈ dom ∧ )) |
9 | 8 | simprd 496 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∧ ) |
10 | 1, 2, 3, 4, 5, 6, 9 | lemeet2 17625 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 = wceq 1528 ∈ wcel 2105 〈cop 4563 class class class wbr 5057 dom cdm 5548 ‘cfv 6348 (class class class)co 7145 Basecbs 16471 lecple 16560 joincjn 17542 meetcmee 17543 Latclat 17643 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-rep 5181 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-reu 3142 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-riota 7103 df-ov 7148 df-oprab 7149 df-glb 17573 df-meet 17575 df-lat 17644 |
This theorem is referenced by: latmlem1 17679 latledi 17687 mod1ile 17703 oldmm1 36233 olm01 36252 cmtcomlemN 36264 cmtbr4N 36271 meetat 36312 cvrexchlem 36435 cvrat4 36459 2llnmj 36576 2lplnmj 36638 dalem25 36714 dalem54 36742 dalem57 36745 cdlema1N 36807 cdlemb 36810 llnexchb2lem 36884 llnexch2N 36886 dalawlem1 36887 dalawlem3 36889 pl42lem1N 36995 lhpelim 37053 lhpat3 37062 4atexlemunv 37082 4atexlemtlw 37083 4atexlemnclw 37086 4atexlemex2 37087 lautm 37110 trlle 37200 cdlemc2 37208 cdlemc5 37211 cdlemd2 37215 cdleme0b 37228 cdleme0c 37229 cdleme0fN 37234 cdleme01N 37237 cdleme0ex1N 37239 cdleme2 37244 cdleme3b 37245 cdleme3c 37246 cdleme3g 37250 cdleme3h 37251 cdleme7aa 37258 cdleme7c 37261 cdleme7d 37262 cdleme7e 37263 cdleme7ga 37264 cdleme11fN 37280 cdleme11k 37284 cdleme15d 37293 cdleme16f 37299 cdlemednpq 37315 cdleme19c 37321 cdleme20aN 37325 cdleme20c 37327 cdleme20j 37334 cdleme21c 37343 cdleme21ct 37345 cdleme22cN 37358 cdleme22f 37362 cdleme23a 37365 cdleme28a 37386 cdleme35d 37468 cdleme35f 37470 cdlemeg46frv 37541 cdlemeg46rgv 37544 cdlemeg46req 37545 cdlemg2fv2 37616 cdlemg2m 37620 cdlemg4 37633 cdlemg10bALTN 37652 cdlemg31b 37714 trlcolem 37742 cdlemk14 37870 dia2dimlem1 38080 docaclN 38140 doca2N 38142 djajN 38153 dihjustlem 38232 dihord1 38234 dihord2a 38235 dihord2b 38236 dihord2cN 38237 dihord11b 38238 dihord11c 38240 dihord2pre 38241 dihlsscpre 38250 dihvalcq2 38263 dihopelvalcpre 38264 dihord6apre 38272 dihord5b 38275 dihord5apre 38278 dihmeetlem1N 38306 dihglblem5apreN 38307 dihglblem3N 38311 dihmeetbclemN 38320 dihmeetlem4preN 38322 dihmeetlem7N 38326 dihmeetlem9N 38331 dihjatcclem4 38437 |
Copyright terms: Public domain | W3C validator |