![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatlej2 | Structured version Visualization version GIF version |
Description: A join's second argument is less than or equal to the join. Special case of latlej2 18386 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 |
---|---|
hlatlej2 | ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlatlej.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
2 | hlatlej.j | . . . 4 ⊢ ∨ = (join‘𝐾) | |
3 | hlatlej.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 1, 2, 3 | hlatlej1 38114 | . . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑃)) |
5 | 4 | 3com23 1126 | . 2 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑃)) |
6 | 2, 3 | hlatjcom 38107 | . 2 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃)) |
7 | 5, 6 | breqtrrd 5170 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 class class class wbr 5142 ‘cfv 6533 (class class class)co 7394 lecple 17188 joincjn 18248 Atomscatm 38002 HLchlt 38089 |
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 5279 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 |
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 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5568 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7350 df-ov 7397 df-oprab 7398 df-lub 18283 df-join 18285 df-lat 18369 df-ats 38006 df-atl 38037 df-cvlat 38061 df-hlat 38090 |
This theorem is referenced by: 2llnne2N 38148 cvrat3 38182 cvrat4 38183 hlatexch3N 38220 hlatexch4 38221 dalem3 38404 dalem25 38438 lnatexN 38519 lncmp 38523 2llnma3r 38528 paddasslem5 38564 dalawlem3 38613 dalawlem6 38616 dalawlem7 38617 dalawlem12 38622 lhp2atne 38774 lhp2at0ne 38776 4atexlemunv 38806 cdlemc2 38932 cdlemc5 38935 cdleme3h 38975 cdleme7 38989 cdleme9 38993 cdleme11c 39001 cdleme11dN 39002 cdleme11j 39007 cdleme16b 39019 cdleme17b 39027 cdleme18a 39031 cdleme18b 39032 cdleme18c 39033 cdleme19a 39043 cdleme20d 39052 cdleme20j 39058 cdleme21ct 39069 cdleme22a 39080 cdleme22e 39084 cdleme22eALTN 39085 cdleme35b 39190 cdlemg9a 39372 cdlemg12a 39383 cdlemg13a 39391 cdlemg17a 39401 cdlemg17g 39407 cdlemg18c 39420 cdlemg33b0 39441 cdlemg46 39475 cdlemh1 39555 cdlemh 39557 cdlemk4 39574 cdlemki 39581 cdlemksv2 39587 cdlemk12 39590 cdlemk15 39595 cdlemk12u 39612 cdlemkid1 39662 dia2dimlem1 39804 dia2dimlem3 39806 cdlemn10 39946 dihjatcclem1 40158 |
Copyright terms: Public domain | W3C validator |