MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latjcom Structured version   Visualization version   GIF version

Theorem latjcom 17664
Description: The join of a lattice commutes. (chjcom 29216 analog.) (Contributed by NM, 16-Sep-2011.)
Hypotheses
Ref Expression
latjcom.b 𝐵 = (Base‘𝐾)
latjcom.j = (join‘𝐾)
Assertion
Ref Expression
latjcom ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑌 𝑋))

Proof of Theorem latjcom
StepHypRef Expression
1 opelxpi 5591 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
213adant1 1124 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
3 latjcom.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 latjcom.j . . . . . . 7 = (join‘𝐾)
5 eqid 2826 . . . . . . 7 (meet‘𝐾) = (meet‘𝐾)
63, 4, 5islat 17652 . . . . . 6 (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))))
7 simprl 767 . . . . . 6 ((𝐾 ∈ Poset ∧ (dom = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))) → dom = (𝐵 × 𝐵))
86, 7sylbi 218 . . . . 5 (𝐾 ∈ Lat → dom = (𝐵 × 𝐵))
983ad2ant1 1127 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → dom = (𝐵 × 𝐵))
102, 9eleqtrrd 2921 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
11 opelxpi 5591 . . . . . 6 ((𝑌𝐵𝑋𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1211ancoms 459 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
13123adant1 1124 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1413, 9eleqtrrd 2921 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ dom )
1510, 14jca 512 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom ))
16 latpos 17655 . . 3 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
173, 4joincom 17635 . . 3 (((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1816, 17syl3anl1 1406 . 2 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1915, 18mpdan 683 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑌 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081   = wceq 1530  wcel 2107  cop 4570   × cxp 5552  dom cdm 5554  cfv 6354  (class class class)co 7150  Basecbs 16478  Posetcpo 17545  joincjn 17549  meetcmee 17550  Latclat 17650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-lub 17579  df-join 17581  df-lat 17651
This theorem is referenced by:  latleeqj2  17669  latjlej2  17671  latnle  17690  latmlej12  17696  latj12  17701  latj32  17702  latj13  17703  latj31  17704  latj4rot  17707  mod2ile  17711  latdisdlem  17794  olj02  36248  omllaw4  36268  cmt2N  36272  cmtbr3N  36276  cvlexch2  36351  cvlexchb2  36353  cvlatexchb2  36357  cvlatexch2  36359  cvlatexch3  36360  cvlatcvr2  36364  cvlsupr2  36365  cvlsupr7  36370  cvlsupr8  36371  hlatjcom  36390  hlrelat5N  36423  cvrval5  36437  cvrexch  36442  cvratlem  36443  cvrat  36444  2atlt  36461  cvrat3  36464  cvrat4  36465  cvrat42  36466  4noncolr3  36475  1cvrat  36498  3atlem1  36505  4atlem4d  36624  4atlem12  36634  paddcom  36835  paddasslem2  36843  pmapjat2  36876  atmod2i1  36883  atmod2i2  36884  llnmod2i2  36885  atmod4i1  36888  atmod4i2  36889  dalawlem4  36896  dalawlem9  36901  dalawlem12  36904  lhpjat2  37043  lhple  37064  trljat1  37188  trljat2  37189  cdlemc1  37213  cdlemc6  37218  cdlemd1  37220  cdleme5  37262  cdleme9  37275  cdleme10  37276  cdleme19e  37329  trlcolem  37748  trljco2  37763  cdlemk7  37870  cdlemk7u  37892  cdlemkid1  37944  dih1  38308  dihjatc2N  38334
  Copyright terms: Public domain W3C validator