![]() |
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 28708 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 17258 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
5 | 4 | adantr 466 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset) |
6 | simpr1 1233 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | |
7 | simpr2 1235 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | |
8 | simpr3 1237 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | |
9 | eqid 2771 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
10 | simpl 468 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat) | |
11 | 1, 3, 9, 10, 6, 7 | latcl2 17256 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom (meet‘𝐾))) |
12 | 11 | simpld 482 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
13 | 1, 2, 3, 5, 6, 7, 8, 12 | joinle 17222 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 〈cop 4322 class class class wbr 4786 dom cdm 5249 ‘cfv 6031 (class class class)co 6793 Basecbs 16064 lecple 16156 Posetcpo 17148 joincjn 17152 meetcmee 17153 Latclat 17253 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-riota 6754 df-ov 6796 df-oprab 6797 df-poset 17154 df-lub 17182 df-join 17184 df-lat 17254 |
This theorem is referenced by: latleeqj1 17271 latjlej1 17273 latjidm 17282 latledi 17297 latjass 17303 mod1ile 17313 lubun 17331 oldmm1 35026 olj01 35034 cvlexchb1 35139 cvlcvr1 35148 hlrelat 35210 hlrelat2 35211 exatleN 35212 hlrelat3 35220 cvrexchlem 35227 cvratlem 35229 cvrat 35230 atlelt 35246 ps-1 35285 hlatexch3N 35288 hlatexch4 35289 3atlem1 35291 3atlem2 35292 lplnexllnN 35372 2llnjaN 35374 4atlem3 35404 4atlem10 35414 4atlem11b 35416 4atlem11 35417 4atlem12b 35419 4atlem12 35420 2lplnja 35427 dalem1 35467 dalem3 35472 dalem8 35478 dalem16 35487 dalem17 35488 dalem21 35502 dalem25 35506 dalem39 35519 dalem54 35534 dalem60 35540 linepsubN 35560 pmapsub 35576 lneq2at 35586 2llnma3r 35596 cdlema1N 35599 cdlemblem 35601 paddasslem5 35632 paddasslem12 35639 paddasslem13 35640 llnexchb2 35677 dalawlem3 35681 dalawlem5 35683 dalawlem8 35686 dalawlem11 35689 dalawlem12 35690 lhp2lt 35809 lhpexle2lem 35817 lhpexle3lem 35819 4atexlemtlw 35875 4atexlemnclw 35878 lautj 35901 cdlemd3 36009 cdleme3g 36043 cdleme3h 36044 cdleme7d 36055 cdleme11c 36070 cdleme15d 36086 cdleme17b 36096 cdleme19a 36112 cdleme20j 36127 cdleme21c 36136 cdleme22b 36150 cdleme22d 36152 cdleme28a 36179 cdleme35a 36257 cdleme35fnpq 36258 cdleme35b 36259 cdleme35f 36263 cdleme42c 36281 cdleme42i 36292 cdlemf1 36370 cdlemg4c 36421 cdlemg6c 36429 cdlemg8b 36437 cdlemg10 36450 cdlemg11b 36451 cdlemg13a 36460 cdlemg17a 36470 cdlemg18b 36488 cdlemg27a 36501 cdlemg33b0 36510 cdlemg35 36522 cdlemg42 36538 cdlemg46 36544 trljco 36549 tendopltp 36589 cdlemk3 36642 cdlemk10 36652 cdlemk1u 36668 cdlemk39 36725 dialss 36856 dia2dimlem1 36874 dia2dimlem10 36883 dia2dimlem12 36885 cdlemm10N 36928 djajN 36947 diblss 36980 cdlemn2 37005 dihord2pre2 37036 dib2dim 37053 dih2dimb 37054 dih2dimbALTN 37055 dihmeetlem6 37119 dihjatcclem1 37228 |
Copyright terms: Public domain | W3C validator |