Theorem hlatjcom 36531

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6336  (class class class)co 7137  Basecbs 16461  joincjn 17532  Latclat 17633  Atomscatm 36426  HLchlt 36513

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 2792  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7442

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 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3012  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3483  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7095  df-ov 7140  df-oprab 7141  df-lub 17562  df-join 17564  df-lat 17634  df-ats 36430  df-atl 36461  df-cvlat 36485  df-hlat 36514

This theorem is referenced by:  hlatj12  36534  hlatjrot  36536  hlatlej2  36539  atbtwnex  36611  3noncolr2  36612  hlatcon2  36615  3dimlem2  36622  3dimlem3  36624  3dimlem3OLDN  36625  3dimlem4  36627  3dimlem4OLDN  36628  ps-1  36640  hlatexch4  36644  lplnribN  36714  4atlem10  36769  4atlem11  36772  dalemswapyz  36819  dalem-cly  36834  dalemswapyzps  36853  dalem24  36860  dalem25  36861  dalem44  36879  2llnma1  36950  2llnma3r  36951  2llnma2rN  36953  llnexchb2  37032  dalawlem4  37037  dalawlem5  37038  dalawlem9  37042  dalawlem11  37044  dalawlem12  37045  dalawlem15  37048  4atexlemex2  37234  4atexlemcnd  37235  ltrncnv  37309  trlcnv  37328  cdlemc6  37359  cdleme7aa  37405  cdleme12  37434  cdleme15a  37437  cdleme15c  37439  cdleme17c  37451  cdlemeda  37461  cdleme19a  37466  cdleme19e  37470  cdleme20bN  37473  cdleme20g  37478  cdleme20m  37486  cdleme21c  37490  cdleme22f  37509  cdleme22g  37511  cdleme35b  37613  cdleme35f  37617  cdleme37m  37625  cdleme39a  37628  cdleme42h  37645  cdleme43aN  37652  cdleme43bN  37653  cdleme43dN  37655  cdleme46f2g2  37656  cdleme46f2g1  37657  cdlemeg46c  37676  cdlemeg46nlpq  37680  cdlemeg46ngfr  37681  cdlemeg46rgv  37691  cdlemeg46gfv  37693  cdlemg2kq  37765  cdlemg4a  37771  cdlemg4d  37776  cdlemg4  37780  cdlemg8c  37792  cdlemg11aq  37801  cdlemg10a  37803  cdlemg12g  37812  cdlemg12  37813  cdlemg13  37815  cdlemg17pq  37835  cdlemg18b  37842  cdlemg18c  37843  cdlemg19  37847  cdlemg21  37849  cdlemk7  38011  cdlemk7u  38033  cdlemkfid1N  38084  dia2dimlem1  38227  dia2dimlem3  38229  dihjatcclem3  38583  dihjat  38586