Theorem hlatjcom 39361

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  joincjn 18272  Latclat 18390  Atomscatm 39256  HLchlt 39343

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 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-lub 18305  df-join 18307  df-lat 18391  df-ats 39260  df-atl 39291  df-cvlat 39315  df-hlat 39344

This theorem is referenced by:  hlatj12  39364  hlatjrot  39366  hlatlej2  39369  atbtwnex  39442  3noncolr2  39443  hlatcon2  39446  3dimlem2  39453  3dimlem3  39455  3dimlem3OLDN  39456  3dimlem4  39458  3dimlem4OLDN  39459  ps-1  39471  hlatexch4  39475  lplnribN  39545  4atlem10  39600  4atlem11  39603  dalemswapyz  39650  dalem-cly  39665  dalemswapyzps  39684  dalem24  39691  dalem25  39692  dalem44  39710  2llnma1  39781  2llnma3r  39782  2llnma2rN  39784  llnexchb2  39863  dalawlem4  39868  dalawlem5  39869  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  dalawlem15  39879  4atexlemex2  40065  4atexlemcnd  40066  ltrncnv  40140  trlcnv  40159  cdlemc6  40190  cdleme7aa  40236  cdleme12  40265  cdleme15a  40268  cdleme15c  40270  cdleme17c  40282  cdlemeda  40292  cdleme19a  40297  cdleme19e  40301  cdleme20bN  40304  cdleme20g  40309  cdleme20m  40317  cdleme21c  40321  cdleme22f  40340  cdleme22g  40342  cdleme35b  40444  cdleme35f  40448  cdleme37m  40456  cdleme39a  40459  cdleme42h  40476  cdleme43aN  40483  cdleme43bN  40484  cdleme43dN  40486  cdleme46f2g2  40487  cdleme46f2g1  40488  cdlemeg46c  40507  cdlemeg46nlpq  40511  cdlemeg46ngfr  40512  cdlemeg46rgv  40522  cdlemeg46gfv  40524  cdlemg2kq  40596  cdlemg4a  40602  cdlemg4d  40607  cdlemg4  40611  cdlemg8c  40623  cdlemg11aq  40632  cdlemg10a  40634  cdlemg12g  40643  cdlemg12  40644  cdlemg13  40646  cdlemg17pq  40666  cdlemg18b  40673  cdlemg18c  40674  cdlemg19  40678  cdlemg21  40680  cdlemk7  40842  cdlemk7u  40864  cdlemkfid1N  40915  dia2dimlem1  41058  dia2dimlem3  41060  dihjatcclem3  41414  dihjat  41417