Theorem hlatjcom 39368

Description: Commutatitivity of join operation. Frequently-used special case of latjcom 18413 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 39363	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		eqid 2730	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		hlatjcom.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39289	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾))
5	2, 3	atbase 39289	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ (Base‘𝐾))
6		hlatjcom.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcom 18413	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
8	1, 4, 5, 7	syl3an 1160	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  joincjn 18279  Latclat 18397  Atomscatm 39263  HLchlt 39350

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-lub 18312  df-join 18314  df-lat 18398  df-ats 39267  df-atl 39298  df-cvlat 39322  df-hlat 39351

This theorem is referenced by:  hlatj12  39371  hlatjrot  39373  hlatlej2  39376  atbtwnex  39449  3noncolr2  39450  hlatcon2  39453  3dimlem2  39460  3dimlem3  39462  3dimlem3OLDN  39463  3dimlem4  39465  3dimlem4OLDN  39466  ps-1  39478  hlatexch4  39482  lplnribN  39552  4atlem10  39607  4atlem11  39610  dalemswapyz  39657  dalem-cly  39672  dalemswapyzps  39691  dalem24  39698  dalem25  39699  dalem44  39717  2llnma1  39788  2llnma3r  39789  2llnma2rN  39791  llnexchb2  39870  dalawlem4  39875  dalawlem5  39876  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  dalawlem15  39886  4atexlemex2  40072  4atexlemcnd  40073  ltrncnv  40147  trlcnv  40166  cdlemc6  40197  cdleme7aa  40243  cdleme12  40272  cdleme15a  40275  cdleme15c  40277  cdleme17c  40289  cdlemeda  40299  cdleme19a  40304  cdleme19e  40308  cdleme20bN  40311  cdleme20g  40316  cdleme20m  40324  cdleme21c  40328  cdleme22f  40347  cdleme22g  40349  cdleme35b  40451  cdleme35f  40455  cdleme37m  40463  cdleme39a  40466  cdleme42h  40483  cdleme43aN  40490  cdleme43bN  40491  cdleme43dN  40493  cdleme46f2g2  40494  cdleme46f2g1  40495  cdlemeg46c  40514  cdlemeg46nlpq  40518  cdlemeg46ngfr  40519  cdlemeg46rgv  40529  cdlemeg46gfv  40531  cdlemg2kq  40603  cdlemg4a  40609  cdlemg4d  40614  cdlemg4  40618  cdlemg8c  40630  cdlemg11aq  40639  cdlemg10a  40641  cdlemg12g  40650  cdlemg12  40651  cdlemg13  40653  cdlemg17pq  40673  cdlemg18b  40680  cdlemg18c  40681  cdlemg19  40685  cdlemg21  40687  cdlemk7  40849  cdlemk7u  40871  cdlemkfid1N  40922  dia2dimlem1  41065  dia2dimlem3  41067  dihjatcclem3  41421  dihjat  41424