Theorem hlatjcom 38226

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ‘cfv 6540  (class class class)co 7405  Basecbs 17140  joincjn 18260  Latclat 18380  Atomscatm 38121  HLchlt 38208

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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

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 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 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-lub 18295  df-join 18297  df-lat 18381  df-ats 38125  df-atl 38156  df-cvlat 38180  df-hlat 38209

This theorem is referenced by:  hlatj12  38229  hlatjrot  38231  hlatlej2  38234  atbtwnex  38307  3noncolr2  38308  hlatcon2  38311  3dimlem2  38318  3dimlem3  38320  3dimlem3OLDN  38321  3dimlem4  38323  3dimlem4OLDN  38324  ps-1  38336  hlatexch4  38340  lplnribN  38410  4atlem10  38465  4atlem11  38468  dalemswapyz  38515  dalem-cly  38530  dalemswapyzps  38549  dalem24  38556  dalem25  38557  dalem44  38575  2llnma1  38646  2llnma3r  38647  2llnma2rN  38649  llnexchb2  38728  dalawlem4  38733  dalawlem5  38734  dalawlem9  38738  dalawlem11  38740  dalawlem12  38741  dalawlem15  38744  4atexlemex2  38930  4atexlemcnd  38931  ltrncnv  39005  trlcnv  39024  cdlemc6  39055  cdleme7aa  39101  cdleme12  39130  cdleme15a  39133  cdleme15c  39135  cdleme17c  39147  cdlemeda  39157  cdleme19a  39162  cdleme19e  39166  cdleme20bN  39169  cdleme20g  39174  cdleme20m  39182  cdleme21c  39186  cdleme22f  39205  cdleme22g  39207  cdleme35b  39309  cdleme35f  39313  cdleme37m  39321  cdleme39a  39324  cdleme42h  39341  cdleme43aN  39348  cdleme43bN  39349  cdleme43dN  39351  cdleme46f2g2  39352  cdleme46f2g1  39353  cdlemeg46c  39372  cdlemeg46nlpq  39376  cdlemeg46ngfr  39377  cdlemeg46rgv  39387  cdlemeg46gfv  39389  cdlemg2kq  39461  cdlemg4a  39467  cdlemg4d  39472  cdlemg4  39476  cdlemg8c  39488  cdlemg11aq  39497  cdlemg10a  39499  cdlemg12g  39508  cdlemg12  39509  cdlemg13  39511  cdlemg17pq  39531  cdlemg18b  39538  cdlemg18c  39539  cdlemg19  39543  cdlemg21  39545  cdlemk7  39707  cdlemk7u  39729  cdlemkfid1N  39780  dia2dimlem1  39923  dia2dimlem3  39925  dihjatcclem3  40279  dihjat  40282