![]() |
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 18473 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 39061 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
2 | eqid 2726 | . . 3 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
3 | hlatlej.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 38987 | . 2 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
5 | 2, 3 | atbase 38987 | . 2 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
6 | hlatlej.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
7 | hlatlej.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
8 | 2, 6, 7 | latlej1 18473 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
9 | 1, 4, 5, 8 | syl3an 1157 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 class class class wbr 5153 ‘cfv 6554 (class class class)co 7424 Basecbs 17213 lecple 17273 joincjn 18336 Latclat 18456 Atomscatm 38961 HLchlt 39048 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-riota 7380 df-ov 7427 df-oprab 7428 df-lub 18371 df-join 18373 df-lat 18457 df-ats 38965 df-atl 38996 df-cvlat 39020 df-hlat 39049 |
This theorem is referenced by: hlatlej2 39074 cvratlem 39120 cvrat4 39142 ps-2 39177 lplnllnneN 39255 dalem1 39358 lnatexN 39478 lncmp 39482 2atm2atN 39484 2llnma3r 39487 dalawlem3 39572 dalawlem6 39575 dalawlem7 39576 dalawlem12 39581 trlval4 39887 cdlemc5 39894 cdlemc6 39895 cdlemd3 39899 cdleme0cp 39913 cdleme3h 39934 cdleme5 39939 cdleme9 39952 cdleme11c 39960 cdleme15b 39974 cdleme17b 39986 cdleme19a 40002 cdleme20c 40010 cdleme20j 40017 cdleme21c 40026 cdleme22b 40040 cdleme22d 40042 cdleme22e 40043 cdleme22eALTN 40044 cdleme35e 40152 cdleme35f 40153 cdleme42a 40170 cdleme17d2 40194 cdlemeg46req 40228 cdlemg13a 40350 cdlemg17a 40360 cdlemg18b 40378 cdlemg27a 40391 trlcoabs2N 40421 cdlemg42 40428 cdlemk4 40533 cdlemk1u 40558 cdlemk39 40615 dia2dimlem1 40763 dia2dimlem2 40764 dia2dimlem3 40765 cdlemm10N 40817 cdlemn10 40905 dihjatcclem1 41117 |
Copyright terms: Public domain | W3C validator |