Theorem hlatjcom 34654

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

Syntax hints:   → wi 4   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  joincjn 16944  Latclat 17045  Atomscatm 34550  HLchlt 34637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-lub 16974  df-join 16976  df-lat 17046  df-ats 34554  df-atl 34585  df-cvlat 34609  df-hlat 34638

This theorem is referenced by:  hlatj12  34657  hlatjrot  34659  hlatlej2  34662  atbtwnex  34734  3noncolr2  34735  hlatcon2  34738  3dimlem2  34745  3dimlem3  34747  3dimlem3OLDN  34748  3dimlem4  34750  3dimlem4OLDN  34751  ps-1  34763  hlatexch4  34767  lplnribN  34837  4atlem10  34892  4atlem11  34895  dalemswapyz  34942  dalem-cly  34957  dalemswapyzps  34976  dalem24  34983  dalem25  34984  dalem44  35002  2llnma1  35073  2llnma3r  35074  2llnma2rN  35076  llnexchb2  35155  dalawlem4  35160  dalawlem5  35161  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  4atexlemex2  35357  4atexlemcnd  35358  ltrncnv  35432  trlcnv  35452  cdlemc6  35483  cdleme7aa  35529  cdleme12  35558  cdleme15a  35561  cdleme15c  35563  cdleme17c  35575  cdlemeda  35585  cdleme20yOLD  35590  cdleme19a  35591  cdleme19e  35595  cdleme20bN  35598  cdleme20g  35603  cdleme20m  35611  cdleme21c  35615  cdleme22f  35634  cdleme22g  35636  cdleme35b  35738  cdleme35f  35742  cdleme37m  35750  cdleme39a  35753  cdleme42h  35770  cdleme43aN  35777  cdleme43bN  35778  cdleme43dN  35780  cdleme46f2g2  35781  cdleme46f2g1  35782  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemeg46ngfr  35806  cdlemeg46rgv  35816  cdlemeg46gfv  35818  cdlemg2kq  35890  cdlemg4a  35896  cdlemg4d  35901  cdlemg4  35905  cdlemg8c  35917  cdlemg11aq  35926  cdlemg10a  35928  cdlemg12g  35937  cdlemg12  35938  cdlemg13  35940  cdlemg17pq  35960  cdlemg18b  35967  cdlemg18c  35968  cdlemg19  35972  cdlemg21  35974  cdlemk7  36136  cdlemk7u  36158  cdlemkfid1N  36209  dia2dimlem1  36353  dia2dimlem3  36355  dihjatcclem3  36709  dihjat  36712