![]() |
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 17410 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
5 | 4 | adantr 474 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset) |
6 | simpr2 1254 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | |
7 | simpr3 1256 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | |
8 | simpr1 1252 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | |
9 | eqid 2825 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
10 | simpl 476 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat) | |
11 | 1, 9, 3, 10, 6, 7 | latcl2 17408 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (〈𝑌, 𝑍〉 ∈ dom (join‘𝐾) ∧ 〈𝑌, 𝑍〉 ∈ dom ∧ )) |
12 | 11 | simprd 491 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 〈𝑌, 𝑍〉 ∈ dom ∧ ) |
13 | 1, 2, 3, 5, 6, 7, 8, 12 | meetle 17388 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1111 = wceq 1656 ∈ wcel 2164 〈cop 4405 class class class wbr 4875 dom cdm 5346 ‘cfv 6127 (class class class)co 6910 Basecbs 16229 lecple 16319 Posetcpo 17300 joincjn 17304 meetcmee 17305 Latclat 17405 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-rep 4996 ax-sep 5007 ax-nul 5015 ax-pow 5067 ax-pr 5129 ax-un 7214 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-ral 3122 df-rex 3123 df-reu 3124 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-pw 4382 df-sn 4400 df-pr 4402 df-op 4406 df-uni 4661 df-iun 4744 df-br 4876 df-opab 4938 df-mpt 4955 df-id 5252 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-rn 5357 df-res 5358 df-ima 5359 df-iota 6090 df-fun 6129 df-fn 6130 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 df-fv 6135 df-riota 6871 df-ov 6913 df-oprab 6914 df-poset 17306 df-glb 17335 df-meet 17337 df-lat 17406 |
This theorem is referenced by: latleeqm1 17439 latmlem1 17441 latmidm 17446 latledi 17449 mod1ile 17465 oldmm1 35287 olm01 35306 cmtbr4N 35325 atnle 35387 atlatmstc 35389 hlrelat2 35473 cvrval5 35485 cvrexchlem 35489 2atjm 35515 atbtwn 35516 ps-2b 35552 2atm 35597 2llnm4 35640 2llnmeqat 35641 dalemcea 35730 dalem21 35764 dalem54 35796 dalem55 35797 dalem57 35799 2atm2atN 35855 2llnma1b 35856 cdlemblem 35863 dalawlem2 35942 dalawlem3 35943 dalawlem6 35946 dalawlem11 35951 dalawlem12 35952 lhpocnle 36086 lhpmcvr4N 36096 lhpat3 36116 4atexlemcnd 36142 lautm 36164 trlval3 36257 cdlemc5 36265 cdleme3 36307 cdleme7ga 36318 cdleme7 36319 cdleme11k 36338 cdleme16e 36352 cdleme16f 36353 cdlemednpq 36369 cdleme22aa 36409 cdleme22b 36411 cdleme22cN 36412 cdleme23c 36421 cdlemeg46req 36599 cdlemf2 36632 cdlemg10c 36709 cdlemg12f 36718 cdlemg17dALTN 36734 cdlemg19a 36753 cdlemg27b 36766 cdlemi 36890 cdlemk15 36925 cdlemk50 37022 dia2dimlem1 37134 dihopelvalcpre 37318 dihord5b 37329 dihmeetlem1N 37360 dihglblem5apreN 37361 dihglblem2N 37364 dihmeetlem3N 37375 |
Copyright terms: Public domain | W3C validator |