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

Theorem latasymb 14209
Description: A lattice ordering is asymetric. (eqss 3228 analog.) (Contributed by NM, 22-Oct-2011.)
Hypotheses
Ref Expression
latref.b  |-  B  =  ( Base `  K
)
latref.l  |-  .<_  =  ( le `  K )
Assertion
Ref Expression
latasymb  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X  .<_  Y  /\  Y  .<_  X )  <-> 
X  =  Y ) )

Proof of Theorem latasymb
StepHypRef Expression
1 latpos 14204 . 2  |-  ( K  e.  Lat  ->  K  e.  Poset )
2 latref.b . . 3  |-  B  =  ( Base `  K
)
3 latref.l . . 3  |-  .<_  =  ( le `  K )
42, 3posasymb 14135 . 2  |-  ( ( K  e.  Poset  /\  X  e.  B  /\  Y  e.  B )  ->  (
( X  .<_  Y  /\  Y  .<_  X )  <->  X  =  Y ) )
51, 4syl3an1 1215 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X  .<_  Y  /\  Y  .<_  X )  <-> 
X  =  Y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1633    e. wcel 1701   class class class wbr 4060   ` cfv 5292   Basecbs 13195   lecple 13262   Posetcpo 14123   Latclat 14200
This theorem is referenced by:  latasym  14210  latasymd  14212  lubun  14276  lubunNEW  28981  cmtbr4N  29263  cvlexchb1  29338  hlateq  29406  cvratlem  29428  cvrat3  29449  pmap11  29769  cdleme50eq  30548  dia11N  31056  dib11N  31168  dih11  31273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-nul 4186
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-poset 14129  df-lat 14201
  Copyright terms: Public domain W3C validator