Theorem hlatjcom 38541

Description: Commutatitivity of join operation. Frequently-used special case of latjcom 18404 for atoms. (Contributed by NM, 15-Jun-2012.)

Hypotheses

Ref	Expression
hlatjcom.j	⊢ ∨ = (join‘𝐾)
hlatjcom.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
hlatjcom	⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))

Proof of Theorem hlatjcom

Step	Hyp	Ref	Expression
1		hllat 38536	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		eqid 2730	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		hlatjcom.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 38462	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾))
5	2, 3	atbase 38462	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ (Base‘𝐾))
6		hlatjcom.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcom 18404	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
8	1, 4, 5, 7	syl3an 1158	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  (class class class)co 7411  Basecbs 17148  joincjn 18268  Latclat 18388  Atomscatm 38436  HLchlt 38523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  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 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-lub 18303  df-join 18305  df-lat 18389  df-ats 38440  df-atl 38471  df-cvlat 38495  df-hlat 38524

This theorem is referenced by:  hlatj12  38544  hlatjrot  38546  hlatlej2  38549  atbtwnex  38622  3noncolr2  38623  hlatcon2  38626  3dimlem2  38633  3dimlem3  38635  3dimlem3OLDN  38636  3dimlem4  38638  3dimlem4OLDN  38639  ps-1  38651  hlatexch4  38655  lplnribN  38725  4atlem10  38780  4atlem11  38783  dalemswapyz  38830  dalem-cly  38845  dalemswapyzps  38864  dalem24  38871  dalem25  38872  dalem44  38890  2llnma1  38961  2llnma3r  38962  2llnma2rN  38964  llnexchb2  39043  dalawlem4  39048  dalawlem5  39049  dalawlem9  39053  dalawlem11  39055  dalawlem12  39056  dalawlem15  39059  4atexlemex2  39245  4atexlemcnd  39246  ltrncnv  39320  trlcnv  39339  cdlemc6  39370  cdleme7aa  39416  cdleme12  39445  cdleme15a  39448  cdleme15c  39450  cdleme17c  39462  cdlemeda  39472  cdleme19a  39477  cdleme19e  39481  cdleme20bN  39484  cdleme20g  39489  cdleme20m  39497  cdleme21c  39501  cdleme22f  39520  cdleme22g  39522  cdleme35b  39624  cdleme35f  39628  cdleme37m  39636  cdleme39a  39639  cdleme42h  39656  cdleme43aN  39663  cdleme43bN  39664  cdleme43dN  39666  cdleme46f2g2  39667  cdleme46f2g1  39668  cdlemeg46c  39687  cdlemeg46nlpq  39691  cdlemeg46ngfr  39692  cdlemeg46rgv  39702  cdlemeg46gfv  39704  cdlemg2kq  39776  cdlemg4a  39782  cdlemg4d  39787  cdlemg4  39791  cdlemg8c  39803  cdlemg11aq  39812  cdlemg10a  39814  cdlemg12g  39823  cdlemg12  39824  cdlemg13  39826  cdlemg17pq  39846  cdlemg18b  39853  cdlemg18c  39854  cdlemg19  39858  cdlemg21  39860  cdlemk7  40022  cdlemk7u  40044  cdlemkfid1N  40095  dia2dimlem1  40238  dia2dimlem3  40240  dihjatcclem3  40594  dihjat  40597