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 29286 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 1132 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
5 | simp2 1133 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
6 | simp3 1134 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
7 | eqid 2823 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
8 | 1, 3, 7, 4, 5, 6 | latcl2 17660 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom (meet‘𝐾))) |
9 | 8 | simpld 497 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
10 | 1, 2, 3, 4, 5, 6, 9 | lejoin1 17624 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 〈cop 4575 class class class wbr 5068 dom cdm 5557 ‘cfv 6357 (class class class)co 7158 Basecbs 16485 lecple 16574 joincjn 17556 meetcmee 17557 Latclat 17657 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-lub 17586 df-join 17588 df-lat 17658 |
This theorem is referenced by: latjlej1 17677 latnlej 17680 latnlej2 17683 latjidm 17686 latnle 17697 latabs2 17700 latmlej11 17702 latjass 17707 mod1ile 17717 lubun 17735 oldmm1 36355 olj01 36363 omllaw5N 36385 cvlexchb1 36468 cvlsupr2 36481 cvlsupr7 36486 hlatlej1 36513 hlrelat5N 36539 2atjm 36583 2llnmj 36698 lplnexllnN 36702 2llnjaN 36704 2llnm2N 36706 4atlem3a 36735 2lplnja 36757 2lplnm2N 36759 2lplnmj 36760 dalemply 36792 dalemsly 36793 dalem10 36811 dalem13 36814 dalem21 36832 dalem55 36865 2llnma1b 36924 cdlema1N 36929 elpaddn0 36938 paddasslem12 36969 paddasslem13 36970 pmapjoin 36990 dalawlem2 37010 dalawlem7 37015 dalawlem11 37019 dalawlem12 37020 lhpmcvr3 37163 lhpmcvr5N 37165 lhpmcvr6N 37166 lautj 37231 trljat1 37304 cdlemc1 37329 cdlemc4 37332 cdleme1 37365 cdleme8 37388 cdleme11g 37403 cdleme22e 37482 cdleme22eALTN 37483 cdleme23b 37488 cdleme23c 37489 cdleme27N 37507 cdleme30a 37516 cdleme35fnpq 37587 cdleme35b 37588 cdleme35c 37589 cdleme42h 37620 cdleme42i 37621 cdleme48bw 37640 cdlemg2fv2 37738 cdlemg7fvbwN 37745 cdlemg8b 37766 cdlemg11b 37780 trlcolem 37864 trljco 37878 cdlemi1 37956 cdlemk48 38088 cdlemn2 38333 dihjustlem 38354 dihord1 38356 dihord5apre 38400 dihglbcpreN 38438 dihmeetlem3N 38443 dihmeetlem11N 38455 |
Copyright terms: Public domain | W3C validator |