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

Theorem latjcom 14165
Description: The join of a lattice commutes. (chjcom 22085 analog.) (Contributed by NM, 16-Sep-2011.)
Hypotheses
Ref Expression
latjcom.b  |-  B  =  ( Base `  K
)
latjcom.j  |-  .\/  =  ( join `  K )
Assertion
Ref Expression
latjcom  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  =  ( Y 
.\/  X ) )

Proof of Theorem latjcom
StepHypRef Expression
1 latjcom.b . . . 4  |-  B  =  ( Base `  K
)
2 latjcom.j . . . 4  |-  .\/  =  ( join `  K )
31, 2latjcl 14156 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
41, 2latjcl 14156 . . . 4  |-  ( ( K  e.  Lat  /\  Y  e.  B  /\  X  e.  B )  ->  ( Y  .\/  X
)  e.  B )
543com23 1157 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( Y  .\/  X
)  e.  B )
63, 5jca 518 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X  .\/  Y )  e.  B  /\  ( Y  .\/  X )  e.  B ) )
7 latpos 14155 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
81, 2joincom 14136 . . 3  |-  ( ( ( K  e.  Poset  /\  X  e.  B  /\  Y  e.  B )  /\  ( ( X  .\/  Y )  e.  B  /\  ( Y  .\/  X )  e.  B ) )  ->  ( X  .\/  Y )  =  ( Y 
.\/  X ) )
97, 8syl3anl1 1230 . 2  |-  ( ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  /\  ( ( X  .\/  Y )  e.  B  /\  ( Y  .\/  X )  e.  B ) )  ->  ( X  .\/  Y )  =  ( Y 
.\/  X ) )
106, 9mpdan 649 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  =  ( Y 
.\/  X ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   ` cfv 5255  (class class class)co 5858   Basecbs 13148   Posetcpo 14074   joincjn 14078   Latclat 14151
This theorem is referenced by:  latleeqj2  14170  latjlej2  14172  latnle  14191  latmlej12  14197  latj12  14202  latj32  14203  latj13  14204  latj31  14205  latj4rot  14208  mod2ile  14212  latdisdlem  14292  olj02  29416  omllaw4  29436  cmt2N  29440  cmtbr3N  29444  cvlexch2  29519  cvlexchb2  29521  cvlatexchb2  29525  cvlatexch2  29527  cvlatexch3  29528  cvlatcvr2  29532  cvlsupr2  29533  cvlsupr7  29538  cvlsupr8  29539  hlatjcom  29557  hlrelat5N  29590  cvrval5  29604  cvrexch  29609  cvratlem  29610  cvrat  29611  2atlt  29628  cvrat3  29631  cvrat4  29632  cvrat42  29633  4noncolr3  29642  1cvrat  29665  3atlem1  29672  4atlem4d  29791  4atlem12  29801  paddcom  30002  paddasslem2  30010  pmapjat2  30043  atmod2i1  30050  atmod2i2  30051  llnmod2i2  30052  atmod4i1  30055  atmod4i2  30056  dalawlem4  30063  dalawlem9  30068  dalawlem12  30071  lhpjat2  30210  lhple  30231  trljat1  30355  trljat2  30356  cdlemc1  30380  cdlemc6  30385  cdlemd1  30387  cdleme5  30429  cdleme9  30442  cdleme10  30443  cdleme19e  30496  trlcolem  30915  trljco2  30930  cdlemk7  31037  cdlemk7u  31059  cdlemkid1  31111  dih1  31476  dihjatc2N  31502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-join 14110  df-lat 14152
  Copyright terms: Public domain W3C validator