Theorem hlatjcom 40425

Description: Commutatitivity of join operation. Frequently-used special case of latjcom 18621 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 40420	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		eqid 2761	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		hlatjcom.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 40346	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾))
5	2, 3	atbase 40346	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ (Base‘𝐾))
6		hlatjcom.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcom 18621	. 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 2145  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  joincjn 18485  Latclat 18605  Atomscatm 40320  HLchlt 40407

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-lub 18518  df-join 18520  df-lat 18606  df-ats 40324  df-atl 40355  df-cvlat 40379  df-hlat 40408

This theorem is used by:  hlatj12  40428  hlatjrot  40430  hlatlej2  40433  atbtwnex  40505  3noncolr2  40506  hlatcon2  40509  3dimlem2  40516  3dimlem3  40518  3dimlem3OLDN  40519  3dimlem4  40521  3dimlem4OLDN  40522  ps-1  40534  hlatexch4  40538  lplnribN  40608  4atlem10  40663  4atlem11  40666  dalemswapyz  40713  dalem-cly  40728  dalemswapyzps  40747  dalem24  40754  dalem25  40755  dalem44  40773  2llnma1  40844  2llnma3r  40845  2llnma2rN  40847  llnexchb2  40926  dalawlem4  40931  dalawlem5  40932  dalawlem9  40936  dalawlem11  40938  dalawlem12  40939  dalawlem15  40942  4atexlemex2  41128  4atexlemcnd  41129  ltrncnv  41203  trlcnv  41222  cdlemc6  41253  cdleme7aa  41299  cdleme12  41328  cdleme15a  41331  cdleme15c  41333  cdleme17c  41345  cdlemeda  41355  cdleme19a  41360  cdleme19e  41364  cdleme20bN  41367  cdleme20g  41372  cdleme20m  41380  cdleme21c  41384  cdleme22f  41403  cdleme22g  41405  cdleme35b  41507  cdleme35f  41511  cdleme37m  41519  cdleme39a  41522  cdleme42h  41539  cdleme43aN  41546  cdleme43bN  41547  cdleme43dN  41549  cdleme46f2g2  41550  cdleme46f2g1  41551  cdlemeg46c  41570  cdlemeg46nlpq  41574  cdlemeg46ngfr  41575  cdlemeg46rgv  41585  cdlemeg46gfv  41587  cdlemg2kq  41659  cdlemg4a  41665  cdlemg4d  41670  cdlemg4  41674  cdlemg8c  41686  cdlemg11aq  41695  cdlemg10a  41697  cdlemg12g  41706  cdlemg12  41707  cdlemg13  41709  cdlemg17pq  41729  cdlemg18b  41736  cdlemg18c  41737  cdlemg19  41741  cdlemg21  41743  cdlemk7  41905  cdlemk7u  41927  cdlemkfid1N  41978  dia2dimlem1  42121  dia2dimlem3  42123  dihjatcclem3  42477  dihjat  42480