![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latlej1 | Structured version Visualization version GIF version |
Description: A join's first argument is less than or equal to the join. (chub1 30278 analog.) (Contributed by NM, 17-Sep-2011.) |
Ref | Expression |
---|---|
latlej.b | ⊢ 𝐵 = (Base‘𝐾) |
latlej.l | ⊢ ≤ = (le‘𝐾) |
latlej.j | ⊢ ∨ = (join‘𝐾) |
Ref | Expression |
---|---|
latlej1 | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latlej.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | latlej.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | latlej.j | . 2 ⊢ ∨ = (join‘𝐾) | |
4 | simp1 1137 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
5 | simp2 1138 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
6 | simp3 1139 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
7 | eqid 2738 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
8 | 1, 3, 7, 4, 5, 6 | latcl2 18285 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom (meet‘𝐾))) |
9 | 8 | simpld 496 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
10 | 1, 2, 3, 4, 5, 6, 9 | lejoin1 18233 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 〈cop 4591 class class class wbr 5104 dom cdm 5632 ‘cfv 6494 (class class class)co 7352 Basecbs 17043 lecple 17100 joincjn 18160 meetcmee 18161 Latclat 18280 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-rep 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7665 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7308 df-ov 7355 df-oprab 7356 df-lub 18195 df-join 18197 df-lat 18281 |
This theorem is referenced by: latjlej1 18302 latnlej 18305 latnlej2 18308 latjidm 18311 latnle 18322 latabs2 18325 latmlej11 18327 latjass 18332 mod1ile 18342 lubun 18364 oldmm1 37611 olj01 37619 omllaw5N 37641 cvlexchb1 37724 cvlsupr2 37737 cvlsupr7 37742 hlatlej1 37769 hlrelat5N 37796 2atjm 37840 2llnmj 37955 lplnexllnN 37959 2llnjaN 37961 2llnm2N 37963 4atlem3a 37992 2lplnja 38014 2lplnm2N 38016 2lplnmj 38017 dalemply 38049 dalemsly 38050 dalem10 38068 dalem13 38071 dalem21 38089 dalem55 38122 2llnma1b 38181 cdlema1N 38186 elpaddn0 38195 paddasslem12 38226 paddasslem13 38227 pmapjoin 38247 dalawlem2 38267 dalawlem7 38272 dalawlem11 38276 dalawlem12 38277 lhpmcvr3 38420 lhpmcvr5N 38422 lhpmcvr6N 38423 lautj 38488 trljat1 38561 cdlemc1 38586 cdlemc4 38589 cdleme1 38622 cdleme8 38645 cdleme11g 38660 cdleme22e 38739 cdleme22eALTN 38740 cdleme23b 38745 cdleme23c 38746 cdleme27N 38764 cdleme30a 38773 cdleme35fnpq 38844 cdleme35b 38845 cdleme35c 38846 cdleme42h 38877 cdleme42i 38878 cdleme48bw 38897 cdlemg2fv2 38995 cdlemg7fvbwN 39002 cdlemg8b 39023 cdlemg11b 39037 trlcolem 39121 trljco 39135 cdlemi1 39213 cdlemk48 39345 cdlemn2 39590 dihjustlem 39611 dihord1 39613 dihord5apre 39657 dihglbcpreN 39695 dihmeetlem3N 39700 dihmeetlem11N 39712 |
Copyright terms: Public domain | W3C validator |