![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latjle12 | Structured version Visualization version GIF version |
Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 29061 analog.) (Contributed by NM, 17-Sep-2011.) |
Ref | Expression |
---|---|
latlej.b | ⊢ 𝐵 = (Base‘𝐾) |
latlej.l | ⊢ ≤ = (le‘𝐾) |
latlej.j | ⊢ ∨ = (join‘𝐾) |
Ref | Expression |
---|---|
latjle12 | ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latlej.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | latlej.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | latlej.j | . 2 ⊢ ∨ = (join‘𝐾) | |
4 | latpos 17512 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
5 | 4 | adantr 473 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset) |
6 | simpr1 1174 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | |
7 | simpr2 1175 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | |
8 | simpr3 1176 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | |
9 | eqid 2775 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
10 | simpl 475 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat) | |
11 | 1, 3, 9, 10, 6, 7 | latcl2 17510 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom (meet‘𝐾))) |
12 | 11 | simpld 487 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
13 | 1, 2, 3, 5, 6, 7, 8, 12 | joinle 17476 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 〈cop 4445 class class class wbr 4927 dom cdm 5404 ‘cfv 6186 (class class class)co 6974 Basecbs 16333 lecple 16422 Posetcpo 17402 joincjn 17406 meetcmee 17407 Latclat 17507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-rep 5047 ax-sep 5058 ax-nul 5065 ax-pow 5117 ax-pr 5184 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-ral 3090 df-rex 3091 df-reu 3092 df-rab 3094 df-v 3414 df-sbc 3681 df-csb 3786 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-nul 4178 df-if 4349 df-pw 4422 df-sn 4440 df-pr 4442 df-op 4446 df-uni 4711 df-iun 4792 df-br 4928 df-opab 4990 df-mpt 5007 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-riota 6935 df-ov 6977 df-oprab 6978 df-poset 17408 df-lub 17436 df-join 17438 df-lat 17508 |
This theorem is referenced by: latleeqj1 17525 latjlej1 17527 latjidm 17536 latledi 17551 latjass 17557 mod1ile 17567 lubun 17585 oldmm1 35776 olj01 35784 cvlexchb1 35889 cvlcvr1 35898 hlrelat 35961 hlrelat2 35962 exatleN 35963 hlrelat3 35971 cvrexchlem 35978 cvratlem 35980 cvrat 35981 atlelt 35997 ps-1 36036 hlatexch3N 36039 hlatexch4 36040 3atlem1 36042 3atlem2 36043 lplnexllnN 36123 2llnjaN 36125 4atlem3 36155 4atlem10 36165 4atlem11b 36167 4atlem11 36168 4atlem12b 36170 4atlem12 36171 2lplnja 36178 dalem1 36218 dalem3 36223 dalem8 36229 dalem16 36238 dalem17 36239 dalem21 36253 dalem25 36257 dalem39 36270 dalem54 36285 dalem60 36291 linepsubN 36311 pmapsub 36327 lneq2at 36337 2llnma3r 36347 cdlema1N 36350 cdlemblem 36352 paddasslem5 36383 paddasslem12 36390 paddasslem13 36391 llnexchb2 36428 dalawlem3 36432 dalawlem5 36434 dalawlem8 36437 dalawlem11 36440 dalawlem12 36441 lhp2lt 36560 lhpexle2lem 36568 lhpexle3lem 36570 4atexlemtlw 36626 4atexlemnclw 36629 lautj 36652 cdlemd3 36759 cdleme3g 36793 cdleme3h 36794 cdleme7d 36805 cdleme11c 36820 cdleme15d 36836 cdleme17b 36846 cdleme19a 36862 cdleme20j 36877 cdleme21c 36886 cdleme22b 36900 cdleme22d 36902 cdleme28a 36929 cdleme35a 37007 cdleme35fnpq 37008 cdleme35b 37009 cdleme35f 37013 cdleme42c 37031 cdleme42i 37042 cdlemf1 37120 cdlemg4c 37171 cdlemg6c 37179 cdlemg8b 37187 cdlemg10 37200 cdlemg11b 37201 cdlemg13a 37210 cdlemg17a 37220 cdlemg18b 37238 cdlemg27a 37251 cdlemg33b0 37260 cdlemg35 37272 cdlemg42 37288 cdlemg46 37294 trljco 37299 tendopltp 37339 cdlemk3 37392 cdlemk10 37402 cdlemk1u 37418 cdlemk39 37475 dialss 37605 dia2dimlem1 37623 dia2dimlem10 37632 dia2dimlem12 37634 cdlemm10N 37677 djajN 37696 diblss 37729 cdlemn2 37754 dihord2pre2 37785 dib2dim 37802 dih2dimb 37803 dih2dimbALTN 37804 dihmeetlem6 37868 dihjatcclem1 37977 |
Copyright terms: Public domain | W3C validator |