![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latlej2 | Structured version Visualization version GIF version |
Description: A join's second argument is less than or equal to the join. (chub2 28884 analog.) (Contributed by NM, 17-Sep-2011.) |
Ref | Expression |
---|---|
latlej.b | ⊢ 𝐵 = (Base‘𝐾) |
latlej.l | ⊢ ≤ = (le‘𝐾) |
latlej.j | ⊢ ∨ = (join‘𝐾) |
Ref | Expression |
---|---|
latlej2 | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ≤ (𝑋 ∨ 𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latlej.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | latlej.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | latlej.j | . 2 ⊢ ∨ = (join‘𝐾) | |
4 | simp1 1167 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
5 | simp2 1168 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
6 | simp3 1169 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
7 | eqid 2797 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
8 | 1, 3, 7, 4, 5, 6 | latcl2 17360 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom (meet‘𝐾))) |
9 | 8 | simpld 489 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
10 | 1, 2, 3, 4, 5, 6, 9 | lejoin2 17325 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ≤ (𝑋 ∨ 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 〈cop 4372 class class class wbr 4841 dom cdm 5310 ‘cfv 6099 (class class class)co 6876 Basecbs 16181 lecple 16271 joincjn 17256 meetcmee 17257 Latclat 17357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-ral 3092 df-rex 3093 df-reu 3094 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-iun 4710 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-riota 6837 df-ov 6879 df-oprab 6880 df-lub 17286 df-join 17288 df-lat 17358 |
This theorem is referenced by: latleeqj1 17375 latjlej1 17377 latnlej 17380 latnlej2 17383 latjass 17407 lubun 17435 oldmm1 35230 cmtcomlemN 35261 cmtbr4N 35268 cvlexchb1 35343 cvlatexch1 35349 cvrval5 35428 2llnjaN 35579 4atlem3b 35611 2lplnja 35632 dalem5 35680 dalem17 35693 dalem39 35724 dalem43 35728 elpaddn0 35813 pmapjoin 35865 dalawlem2 35885 dalawlem11 35894 dalawlem12 35895 lautj 36106 trljat2 36180 cdleme0cq 36228 cdleme1 36240 cdleme3 36250 cdleme5 36253 cdleme7ga 36261 cdleme10 36267 cdleme15b 36288 cdleme16b 36292 cdleme20k 36332 cdleme22e 36357 cdleme22eALTN 36358 cdleme23c 36364 cdleme28a 36383 cdleme32e 36458 cdleme35a 36461 cdlemg4c 36625 cdlemg6c 36633 trlcolem 36739 cdlemi1 36831 dia2dimlem2 37078 cdlemm10N 37131 dihord2pre2 37239 dihord5apre 37275 dihjatc1 37324 |
Copyright terms: Public domain | W3C validator |