Theorem hlatjcom 40202

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7419  Basecbs 17293  joincjn 18391  Latclat 18511  Atomscatm 40097  HLchlt 40184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-lub 18424  df-join 18426  df-lat 18512  df-ats 40101  df-atl 40132  df-cvlat 40156  df-hlat 40185

This theorem is used by:  hlatj12  40205  hlatjrot  40207  hlatlej2  40210  atbtwnex  40282  3noncolr2  40283  hlatcon2  40286  3dimlem2  40293  3dimlem3  40295  3dimlem3OLDN  40296  3dimlem4  40298  3dimlem4OLDN  40299  ps-1  40311  hlatexch4  40315  lplnribN  40385  4atlem10  40440  4atlem11  40443  dalemswapyz  40490  dalem-cly  40505  dalemswapyzps  40524  dalem24  40531  dalem25  40532  dalem44  40550  2llnma1  40621  2llnma3r  40622  2llnma2rN  40624  llnexchb2  40703  dalawlem4  40708  dalawlem5  40709  dalawlem9  40713  dalawlem11  40715  dalawlem12  40716  dalawlem15  40719  4atexlemex2  40905  4atexlemcnd  40906  ltrncnv  40980  trlcnv  40999  cdlemc6  41030  cdleme7aa  41076  cdleme12  41105  cdleme15a  41108  cdleme15c  41110  cdleme17c  41122  cdlemeda  41132  cdleme19a  41137  cdleme19e  41141  cdleme20bN  41144  cdleme20g  41149  cdleme20m  41157  cdleme21c  41161  cdleme22f  41180  cdleme22g  41182  cdleme35b  41284  cdleme35f  41288  cdleme37m  41296  cdleme39a  41299  cdleme42h  41316  cdleme43aN  41323  cdleme43bN  41324  cdleme43dN  41326  cdleme46f2g2  41327  cdleme46f2g1  41328  cdlemeg46c  41347  cdlemeg46nlpq  41351  cdlemeg46ngfr  41352  cdlemeg46rgv  41362  cdlemeg46gfv  41364  cdlemg2kq  41436  cdlemg4a  41442  cdlemg4d  41447  cdlemg4  41451  cdlemg8c  41463  cdlemg11aq  41472  cdlemg10a  41474  cdlemg12g  41483  cdlemg12  41484  cdlemg13  41486  cdlemg17pq  41506  cdlemg18b  41513  cdlemg18c  41514  cdlemg19  41518  cdlemg21  41520  cdlemk7  41682  cdlemk7u  41704  cdlemkfid1N  41755  dia2dimlem1  41898  dia2dimlem3  41900  dihjatcclem3  42254  dihjat  42257