![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatlej1 | Structured version Visualization version GIF version |
Description: A join's first argument is less than or equal to the join. Special case of latlej1 18397 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
Ref | Expression |
---|---|
hlatlej.l | β’ β€ = (leβπΎ) |
hlatlej.j | β’ β¨ = (joinβπΎ) |
hlatlej.a | β’ π΄ = (AtomsβπΎ) |
Ref | Expression |
---|---|
hlatlej1 | β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hllat 38221 | . 2 β’ (πΎ β HL β πΎ β Lat) | |
2 | eqid 2732 | . . 3 β’ (BaseβπΎ) = (BaseβπΎ) | |
3 | hlatlej.a | . . 3 β’ π΄ = (AtomsβπΎ) | |
4 | 2, 3 | atbase 38147 | . 2 β’ (π β π΄ β π β (BaseβπΎ)) |
5 | 2, 3 | atbase 38147 | . 2 β’ (π β π΄ β π β (BaseβπΎ)) |
6 | hlatlej.l | . . 3 β’ β€ = (leβπΎ) | |
7 | hlatlej.j | . . 3 β’ β¨ = (joinβπΎ) | |
8 | 2, 6, 7 | latlej1 18397 | . 2 β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β π β€ (π β¨ π)) |
9 | 1, 4, 5, 8 | syl3an 1160 | 1 β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ w3a 1087 = wceq 1541 β wcel 2106 class class class wbr 5147 βcfv 6540 (class class class)co 7405 Basecbs 17140 lecple 17200 joincjn 18260 Latclat 18380 Atomscatm 38121 HLchlt 38208 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-lub 18295 df-join 18297 df-lat 18381 df-ats 38125 df-atl 38156 df-cvlat 38180 df-hlat 38209 |
This theorem is referenced by: hlatlej2 38234 cvratlem 38280 cvrat4 38302 ps-2 38337 lplnllnneN 38415 dalem1 38518 lnatexN 38638 lncmp 38642 2atm2atN 38644 2llnma3r 38647 dalawlem3 38732 dalawlem6 38735 dalawlem7 38736 dalawlem12 38741 trlval4 39047 cdlemc5 39054 cdlemc6 39055 cdlemd3 39059 cdleme0cp 39073 cdleme3h 39094 cdleme5 39099 cdleme9 39112 cdleme11c 39120 cdleme15b 39134 cdleme17b 39146 cdleme19a 39162 cdleme20c 39170 cdleme20j 39177 cdleme21c 39186 cdleme22b 39200 cdleme22d 39202 cdleme22e 39203 cdleme22eALTN 39204 cdleme35e 39312 cdleme35f 39313 cdleme42a 39330 cdleme17d2 39354 cdlemeg46req 39388 cdlemg13a 39510 cdlemg17a 39520 cdlemg18b 39538 cdlemg27a 39551 trlcoabs2N 39581 cdlemg42 39588 cdlemk4 39693 cdlemk1u 39718 cdlemk39 39775 dia2dimlem1 39923 dia2dimlem2 39924 dia2dimlem3 39925 cdlemm10N 39977 cdlemn10 40065 dihjatcclem1 40277 |
Copyright terms: Public domain | W3C validator |