![]() |
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 1129 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
5 | simp2 1130 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
6 | simp3 1131 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
7 | eqid 2795 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
8 | 1, 7, 3, 4, 5, 6 | latcl2 17487 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom (join‘𝐾) ∧ 〈𝑋, 𝑌〉 ∈ dom ∧ )) |
9 | 8 | simprd 496 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∧ ) |
10 | 1, 2, 3, 4, 5, 6, 9 | lemeet2 17466 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 〈cop 4478 class class class wbr 4962 dom cdm 5443 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 lecple 16401 joincjn 17383 meetcmee 17384 Latclat 17484 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-glb 17414 df-meet 17416 df-lat 17485 |
This theorem is referenced by: latmlem1 17520 latledi 17528 mod1ile 17544 oldmm1 35884 olm01 35903 cmtcomlemN 35915 cmtbr4N 35922 meetat 35963 cvrexchlem 36086 cvrat4 36110 2llnmj 36227 2lplnmj 36289 dalem25 36365 dalem54 36393 dalem57 36396 cdlema1N 36458 cdlemb 36461 llnexchb2lem 36535 llnexch2N 36537 dalawlem1 36538 dalawlem3 36540 pl42lem1N 36646 lhpelim 36704 lhpat3 36713 4atexlemunv 36733 4atexlemtlw 36734 4atexlemnclw 36737 4atexlemex2 36738 lautm 36761 trlle 36851 cdlemc2 36859 cdlemc5 36862 cdlemd2 36866 cdleme0b 36879 cdleme0c 36880 cdleme0fN 36885 cdleme01N 36888 cdleme0ex1N 36890 cdleme2 36895 cdleme3b 36896 cdleme3c 36897 cdleme3g 36901 cdleme3h 36902 cdleme7aa 36909 cdleme7c 36912 cdleme7d 36913 cdleme7e 36914 cdleme7ga 36915 cdleme11fN 36931 cdleme11k 36935 cdleme15d 36944 cdleme16f 36950 cdlemednpq 36966 cdleme19c 36972 cdleme20aN 36976 cdleme20c 36978 cdleme20j 36985 cdleme21c 36994 cdleme21ct 36996 cdleme22cN 37009 cdleme22f 37013 cdleme23a 37016 cdleme28a 37037 cdleme35d 37119 cdleme35f 37121 cdlemeg46frv 37192 cdlemeg46rgv 37195 cdlemeg46req 37196 cdlemg2fv2 37267 cdlemg2m 37271 cdlemg4 37284 cdlemg10bALTN 37303 cdlemg31b 37365 trlcolem 37393 cdlemk14 37521 dia2dimlem1 37731 docaclN 37791 doca2N 37793 djajN 37804 dihjustlem 37883 dihord1 37885 dihord2a 37886 dihord2b 37887 dihord2cN 37888 dihord11b 37889 dihord11c 37891 dihord2pre 37892 dihlsscpre 37901 dihvalcq2 37914 dihopelvalcpre 37915 dihord6apre 37923 dihord5b 37926 dihord5apre 37929 dihmeetlem1N 37957 dihglblem5apreN 37958 dihglblem3N 37962 dihmeetbclemN 37971 dihmeetlem4preN 37973 dihmeetlem7N 37977 dihmeetlem9N 37982 dihjatcclem4 38088 |
Copyright terms: Public domain | W3C validator |