| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > latmle1 | Structured version Visualization version GIF version | ||
| Description: A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.) |
| Ref | Expression |
|---|---|
| latmle.b | ⊢ 𝐵 = (Base‘𝐾) |
| latmle.l | ⊢ ≤ = (le‘𝐾) |
| latmle.m | ⊢ ∧ = (meet‘𝐾) |
| Ref | Expression |
|---|---|
| latmle1 | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latmle.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
| 2 | latmle.l | . 2 ⊢ ≤ = (le‘𝐾) | |
| 3 | latmle.m | . 2 ⊢ ∧ = (meet‘𝐾) | |
| 4 | simp1 1149 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
| 5 | simp2 1150 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
| 6 | simp3 1151 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
| 7 | eqid 2762 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
| 8 | 1, 7, 3, 4, 5, 6 | latcl2 18468 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom (join‘𝐾) ∧ 〈𝑋, 𝑌〉 ∈ dom ∧ )) |
| 9 | 8 | simprd 499 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∧ ) |
| 10 | 1, 2, 3, 4, 5, 6, 9 | lemeet1 18428 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 〈cop 4588 class class class wbr 5100 dom cdm 5647 ‘cfv 6521 (class class class)co 7396 Basecbs 17245 lecple 17293 joincjn 18343 meetcmee 18344 Latclat 18463 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5542 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-glb 18377 df-meet 18379 df-lat 18464 |
| This theorem is referenced by: latleeqm1 18499 latmlem1 18501 latnlemlt 18504 latmidm 18506 latabs1 18507 latledi 18509 latmlej11 18510 oldmm1 39838 cmtbr3N 39875 cmtbr4N 39876 lecmtN 39877 cvrat4 40064 2llnmat 40145 llnmlplnN 40160 dalem3 40285 dalem27 40320 dalem54 40347 dalem55 40348 2lnat 40405 cdlema1N 40412 llnexchb2lem 40489 dalawlem1 40492 dalawlem6 40497 dalawlem11 40502 dalawlem12 40503 4atexlemunv 40687 4atexlemc 40690 4atexlemnclw 40691 4atexlemex2 40692 4atexlemcnd 40693 lautm 40715 trlval3 40808 cdlemeulpq 40841 cdleme3h 40856 cdleme4a 40860 cdleme9 40874 cdleme11g 40886 cdleme13 40893 cdleme16e 40903 cdlemednpq 40920 cdleme19b 40925 cdleme20e 40934 cdleme20j 40939 cdleme22cN 40963 cdleme22e 40965 cdleme22eALTN 40966 cdleme22g 40969 cdleme35b 41071 cdleme35f 41075 cdlemeg46vrg 41148 cdlemg11b 41263 cdlemg12f 41269 cdlemg19a 41304 cdlemg31a 41318 cdlemk12 41471 cdlemkole 41474 cdlemk12u 41493 cdlemk37 41535 dia2dimlem1 41685 dihopelvalcpre 41869 dihmeetlem1N 41911 dihglblem5apreN 41912 dihglblem2N 41915 dihmeetlem2N 41920 |
| Copyright terms: Public domain | W3C validator |