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

Theorem atcmp 29794
Description: If two atoms are comparable, they are equal. (atsseq 23803 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 29784 . . 3  |-  ( K  e.  AtLat  ->  K  e.  Poset
)
213ad2ant1 978 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  Q  e.  A )  ->  K  e.  Poset )
3 eqid 2404 . . . 4  |-  ( Base `  K )  =  (
Base `  K )
4 atcmp.a . . . 4  |-  A  =  ( Atoms `  K )
53, 4atbase 29772 . . 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 29772 . . 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 2404 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
103, 9atl0cl 29786 . . 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 2404 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
139, 12, 4atcvr0 29771 . . 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 29771 . . 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 29766 . 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 1721   class class class wbr 4172   ` cfv 5413   Basecbs 13424   lecple 13491   Posetcpo 14352   0.cp0 14421    <o ccvr 29745   Atomscatm 29746   AtLatcal 29747
This theorem is referenced by:  atncmp  29795  atnlt  29796  atnle  29800  cvlsupr2  29826  cvratlem  29903  2atjm  29927  atbtwn  29928  2atm  30009  2llnmeqat  30053  dalem25  30180  dalem55  30209  dalem57  30211  snatpsubN  30232  pmapat  30245  2llnma1b  30268  cdlemblem  30275  lhp2at0nle  30517  lhpat3  30528  4atexlemcnd  30554  trlval3  30669  cdlemc5  30677  cdleme3  30719  cdleme7  30731  cdleme11k  30750  cdleme16b  30761  cdleme16e  30764  cdleme16f  30765  cdlemednpq  30781  cdleme20j  30800  cdleme22aa  30821  cdleme22cN  30824  cdleme22d  30825  cdlemf2  31044  cdlemb3  31088  cdlemg12e  31129  cdlemg17dALTN  31146  cdlemg19a  31165  cdlemg27b  31178  cdlemg31d  31182  trlcone  31210  cdlemi  31302  tendotr  31312  cdlemk17  31340  cdlemk52  31436  cdleml1N  31458  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-ov 6043  df-poset 14358  df-plt 14370  df-lat 14430  df-covers 29749  df-ats 29750  df-atl 29781
  Copyright terms: Public domain W3C validator