Theorem hlatjcom 39992

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

Syntax hints:   → wi 4   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  joincjn 18343  Latclat 18463  Atomscatm 39887  HLchlt 39974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-lub 18376  df-join 18378  df-lat 18464  df-ats 39891  df-atl 39922  df-cvlat 39946  df-hlat 39975

This theorem is referenced by:  hlatj12  39995  hlatjrot  39997  hlatlej2  40000  atbtwnex  40072  3noncolr2  40073  hlatcon2  40076  3dimlem2  40083  3dimlem3  40085  3dimlem3OLDN  40086  3dimlem4  40088  3dimlem4OLDN  40089  ps-1  40101  hlatexch4  40105  lplnribN  40175  4atlem10  40230  4atlem11  40233  dalemswapyz  40280  dalem-cly  40295  dalemswapyzps  40314  dalem24  40321  dalem25  40322  dalem44  40340  2llnma1  40411  2llnma3r  40412  2llnma2rN  40414  llnexchb2  40493  dalawlem4  40498  dalawlem5  40499  dalawlem9  40503  dalawlem11  40505  dalawlem12  40506  dalawlem15  40509  4atexlemex2  40695  4atexlemcnd  40696  ltrncnv  40770  trlcnv  40789  cdlemc6  40820  cdleme7aa  40866  cdleme12  40895  cdleme15a  40898  cdleme15c  40900  cdleme17c  40912  cdlemeda  40922  cdleme19a  40927  cdleme19e  40931  cdleme20bN  40934  cdleme20g  40939  cdleme20m  40947  cdleme21c  40951  cdleme22f  40970  cdleme22g  40972  cdleme35b  41074  cdleme35f  41078  cdleme37m  41086  cdleme39a  41089  cdleme42h  41106  cdleme43aN  41113  cdleme43bN  41114  cdleme43dN  41116  cdleme46f2g2  41117  cdleme46f2g1  41118  cdlemeg46c  41137  cdlemeg46nlpq  41141  cdlemeg46ngfr  41142  cdlemeg46rgv  41152  cdlemeg46gfv  41154  cdlemg2kq  41226  cdlemg4a  41232  cdlemg4d  41237  cdlemg4  41241  cdlemg8c  41253  cdlemg11aq  41262  cdlemg10a  41264  cdlemg12g  41273  cdlemg12  41274  cdlemg13  41276  cdlemg17pq  41296  cdlemg18b  41303  cdlemg18c  41304  cdlemg19  41308  cdlemg21  41310  cdlemk7  41472  cdlemk7u  41494  cdlemkfid1N  41545  dia2dimlem1  41688  dia2dimlem3  41690  dihjatcclem3  42044  dihjat  42047