Theorem hlatjcom 36519

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  joincjn 17554  Latclat 17655  Atomscatm 36414  HLchlt 36501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-lub 17584  df-join 17586  df-lat 17656  df-ats 36418  df-atl 36449  df-cvlat 36473  df-hlat 36502

This theorem is referenced by:  hlatj12  36522  hlatjrot  36524  hlatlej2  36527  atbtwnex  36599  3noncolr2  36600  hlatcon2  36603  3dimlem2  36610  3dimlem3  36612  3dimlem3OLDN  36613  3dimlem4  36615  3dimlem4OLDN  36616  ps-1  36628  hlatexch4  36632  lplnribN  36702  4atlem10  36757  4atlem11  36760  dalemswapyz  36807  dalem-cly  36822  dalemswapyzps  36841  dalem24  36848  dalem25  36849  dalem44  36867  2llnma1  36938  2llnma3r  36939  2llnma2rN  36941  llnexchb2  37020  dalawlem4  37025  dalawlem5  37026  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem15  37036  4atexlemex2  37222  4atexlemcnd  37223  ltrncnv  37297  trlcnv  37316  cdlemc6  37347  cdleme7aa  37393  cdleme12  37422  cdleme15a  37425  cdleme15c  37427  cdleme17c  37439  cdlemeda  37449  cdleme19a  37454  cdleme19e  37458  cdleme20bN  37461  cdleme20g  37466  cdleme20m  37474  cdleme21c  37478  cdleme22f  37497  cdleme22g  37499  cdleme35b  37601  cdleme35f  37605  cdleme37m  37613  cdleme39a  37616  cdleme42h  37633  cdleme43aN  37640  cdleme43bN  37641  cdleme43dN  37643  cdleme46f2g2  37644  cdleme46f2g1  37645  cdlemeg46c  37664  cdlemeg46nlpq  37668  cdlemeg46ngfr  37669  cdlemeg46rgv  37679  cdlemeg46gfv  37681  cdlemg2kq  37753  cdlemg4a  37759  cdlemg4d  37764  cdlemg4  37768  cdlemg8c  37780  cdlemg11aq  37789  cdlemg10a  37791  cdlemg12g  37800  cdlemg12  37801  cdlemg13  37803  cdlemg17pq  37823  cdlemg18b  37830  cdlemg18c  37831  cdlemg19  37835  cdlemg21  37837  cdlemk7  37999  cdlemk7u  38021  cdlemkfid1N  38072  dia2dimlem1  38215  dia2dimlem3  38217  dihjatcclem3  38571  dihjat  38574