Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  atcmp Unicode version

Theorem atcmp 29427
Description: If two atoms are comparable, they are equal. (atsseq 23699 analog.) (Contributed by NM, 13-Oct-2011.)
Hypotheses
Ref Expression
atcmp.l  |-  .<_  =  ( le `  K )
atcmp.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
atcmp  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .<_  Q  <->  P  =  Q ) )

Proof of Theorem atcmp
StepHypRef Expression
1 atlpos 29417 . . 3  |-  ( K  e.  AtLat  ->  K  e.  Poset
)
213ad2ant1 978 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  K  e.  Poset )
3 eqid 2388 . . . 4  |-  ( Base `  K )  =  (
Base `  K )
4 atcmp.a . . . 4  |-  A  =  ( Atoms `  K )
53, 4atbase 29405 . . 3  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
653ad2ant2 979 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  P  e.  ( Base `  K
) )
73, 4atbase 29405 . . 3  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
873ad2ant3 980 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  Q  e.  ( Base `  K
) )
9 eqid 2388 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
103, 9atl0cl 29419 . . 3  |-  ( K  e.  AtLat  ->  ( 0. `  K )  e.  (
Base `  K )
)
11103ad2ant1 978 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  ( 0. `  K )  e.  ( Base `  K
) )
12 eqid 2388 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
139, 12, 4atcvr0 29404 . . 3  |-  ( ( K  e.  AtLat  /\  P  e.  A )  ->  ( 0. `  K ) ( 
<o  `  K ) P )
14133adant3 977 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  ( 0. `  K ) ( 
<o  `  K ) P )
159, 12, 4atcvr0 29404 . . 3  |-  ( ( K  e.  AtLat  /\  Q  e.  A )  ->  ( 0. `  K ) ( 
<o  `  K ) Q )
16153adant2 976 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  ( 0. `  K ) ( 
<o  `  K ) Q )
17 atcmp.l . . 3  |-  .<_  =  ( le `  K )
183, 17, 12cvrcmp 29399 . 2  |-  ( ( K  e.  Poset  /\  ( P  e.  ( Base `  K )  /\  Q  e.  ( Base `  K
)  /\  ( 0. `  K )  e.  (
Base `  K )
)  /\  ( ( 0. `  K ) ( 
<o  `  K ) P  /\  ( 0. `  K ) (  <o  `  K ) Q ) )  ->  ( P  .<_  Q  <->  P  =  Q
) )
192, 6, 8, 11, 14, 16, 18syl132anc 1202 1  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .<_  Q  <->  P  =  Q ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936    = wceq 1649    e. wcel 1717   class class class wbr 4154   ` cfv 5395   Basecbs 13397   lecple 13464   Posetcpo 14325   0.cp0 14394    <o ccvr 29378   Atomscatm 29379   AtLatcal 29380
This theorem is referenced by:  atncmp  29428  atnlt  29429  atnle  29433  cvlsupr2  29459  cvratlem  29536  2atjm  29560  atbtwn  29561  2atm  29642  2llnmeqat  29686  dalem25  29813  dalem55  29842  dalem57  29844  snatpsubN  29865  pmapat  29878  2llnma1b  29901  cdlemblem  29908  lhp2at0nle  30150  lhpat3  30161  4atexlemcnd  30187  trlval3  30302  cdlemc5  30310  cdleme3  30352  cdleme7  30364  cdleme11k  30383  cdleme16b  30394  cdleme16e  30397  cdleme16f  30398  cdlemednpq  30414  cdleme20j  30433  cdleme22aa  30454  cdleme22cN  30457  cdleme22d  30458  cdlemf2  30677  cdlemb3  30721  cdlemg12e  30762  cdlemg17dALTN  30779  cdlemg19a  30798  cdlemg27b  30811  cdlemg31d  30815  trlcone  30843  cdlemi  30935  tendotr  30945  cdlemk17  30973  cdlemk52  31069  cdleml1N  31091  dia2dimlem1  31180  dia2dimlem2  31181  dia2dimlem3  31182
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-mpt 4210  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-iota 5359  df-fun 5397  df-fv 5403  df-ov 6024  df-poset 14331  df-plt 14343  df-lat 14403  df-covers 29382  df-ats 29383  df-atl 29414
  Copyright terms: Public domain W3C validator