Theorem hlatjcom 39369

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  joincjn 18357  Latclat 18476  Atomscatm 39264  HLchlt 39351

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-lub 18391  df-join 18393  df-lat 18477  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352

This theorem is referenced by:  hlatj12  39372  hlatjrot  39374  hlatlej2  39377  atbtwnex  39450  3noncolr2  39451  hlatcon2  39454  3dimlem2  39461  3dimlem3  39463  3dimlem3OLDN  39464  3dimlem4  39466  3dimlem4OLDN  39467  ps-1  39479  hlatexch4  39483  lplnribN  39553  4atlem10  39608  4atlem11  39611  dalemswapyz  39658  dalem-cly  39673  dalemswapyzps  39692  dalem24  39699  dalem25  39700  dalem44  39718  2llnma1  39789  2llnma3r  39790  2llnma2rN  39792  llnexchb2  39871  dalawlem4  39876  dalawlem5  39877  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  dalawlem15  39887  4atexlemex2  40073  4atexlemcnd  40074  ltrncnv  40148  trlcnv  40167  cdlemc6  40198  cdleme7aa  40244  cdleme12  40273  cdleme15a  40276  cdleme15c  40278  cdleme17c  40290  cdlemeda  40300  cdleme19a  40305  cdleme19e  40309  cdleme20bN  40312  cdleme20g  40317  cdleme20m  40325  cdleme21c  40329  cdleme22f  40348  cdleme22g  40350  cdleme35b  40452  cdleme35f  40456  cdleme37m  40464  cdleme39a  40467  cdleme42h  40484  cdleme43aN  40491  cdleme43bN  40492  cdleme43dN  40494  cdleme46f2g2  40495  cdleme46f2g1  40496  cdlemeg46c  40515  cdlemeg46nlpq  40519  cdlemeg46ngfr  40520  cdlemeg46rgv  40530  cdlemeg46gfv  40532  cdlemg2kq  40604  cdlemg4a  40610  cdlemg4d  40615  cdlemg4  40619  cdlemg8c  40631  cdlemg11aq  40640  cdlemg10a  40642  cdlemg12g  40651  cdlemg12  40652  cdlemg13  40654  cdlemg17pq  40674  cdlemg18b  40681  cdlemg18c  40682  cdlemg19  40686  cdlemg21  40688  cdlemk7  40850  cdlemk7u  40872  cdlemkfid1N  40923  dia2dimlem1  41066  dia2dimlem3  41068  dihjatcclem3  41422  dihjat  41425