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

Theorem latjcom 17778
Description: The join of a lattice commutes. (chjcom 29433 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 5556 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
213adant1 1131 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
3 latjcom.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 latjcom.j . . . . . . 7 = (join‘𝐾)
5 eqid 2738 . . . . . . 7 (meet‘𝐾) = (meet‘𝐾)
63, 4, 5islat 17766 . . . . . 6 (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))))
7 simprl 771 . . . . . 6 ((𝐾 ∈ Poset ∧ (dom = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))) → dom = (𝐵 × 𝐵))
86, 7sylbi 220 . . . . 5 (𝐾 ∈ Lat → dom = (𝐵 × 𝐵))
983ad2ant1 1134 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → dom = (𝐵 × 𝐵))
102, 9eleqtrrd 2836 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
11 opelxpi 5556 . . . . . 6 ((𝑌𝐵𝑋𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1211ancoms 462 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
13123adant1 1131 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1413, 9eleqtrrd 2836 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ dom )
1510, 14jca 515 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom ))
16 latpos 17769 . . 3 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
173, 4joincom 17749 . . 3 (((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1816, 17syl3anl1 1413 . 2 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1915, 18mpdan 687 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑌 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088   = wceq 1542  wcel 2113  cop 4519   × cxp 5517  dom cdm 5519  cfv 6333  (class class class)co 7164  Basecbs 16579  Posetcpo 17659  joincjn 17663  meetcmee 17664  Latclat 17764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-lub 17693  df-join 17695  df-lat 17765
This theorem is referenced by:  latleeqj2  17783  latjlej2  17785  latnle  17804  latmlej12  17810  latj12  17815  latj32  17816  latj13  17817  latj31  17818  latj4rot  17821  mod2ile  17825  latdisdlem  17908  olj02  36852  omllaw4  36872  cmt2N  36876  cmtbr3N  36880  cvlexch2  36955  cvlexchb2  36957  cvlatexchb2  36961  cvlatexch2  36963  cvlatexch3  36964  cvlatcvr2  36968  cvlsupr2  36969  cvlsupr7  36974  cvlsupr8  36975  hlatjcom  36994  hlrelat5N  37027  cvrval5  37041  cvrexch  37046  cvratlem  37047  cvrat  37048  2atlt  37065  cvrat3  37068  cvrat4  37069  cvrat42  37070  4noncolr3  37079  1cvrat  37102  3atlem1  37109  4atlem4d  37228  4atlem12  37238  paddcom  37439  paddasslem2  37447  pmapjat2  37480  atmod2i1  37487  atmod2i2  37488  llnmod2i2  37489  atmod4i1  37492  atmod4i2  37493  dalawlem4  37500  dalawlem9  37505  dalawlem12  37508  lhpjat2  37647  lhple  37668  trljat1  37792  trljat2  37793  cdlemc1  37817  cdlemc6  37822  cdlemd1  37824  cdleme5  37866  cdleme9  37879  cdleme10  37880  cdleme19e  37933  trlcolem  38352  trljco2  38367  cdlemk7  38474  cdlemk7u  38496  cdlemkid1  38548  dih1  38912  dihjatc2N  38938
  Copyright terms: Public domain W3C validator