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

Theorem atcmp 34078
Description: If two atoms are comparable, they are equal. (atsseq 29055 analog.) (Contributed by NM, 13-Oct-2011.)
Hypotheses
Ref Expression
atcmp.l = (le‘𝐾)
atcmp.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
atcmp ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄𝑃 = 𝑄))

Proof of Theorem atcmp
StepHypRef Expression
1 atlpos 34068 . . 3 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
213ad2ant1 1080 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → 𝐾 ∈ Poset)
3 eqid 2621 . . . 4 (Base‘𝐾) = (Base‘𝐾)
4 atcmp.a . . . 4 𝐴 = (Atoms‘𝐾)
53, 4atbase 34056 . . 3 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
653ad2ant2 1081 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → 𝑃 ∈ (Base‘𝐾))
73, 4atbase 34056 . . 3 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
873ad2ant3 1082 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → 𝑄 ∈ (Base‘𝐾))
9 eqid 2621 . . . 4 (0.‘𝐾) = (0.‘𝐾)
103, 9atl0cl 34070 . . 3 (𝐾 ∈ AtLat → (0.‘𝐾) ∈ (Base‘𝐾))
11103ad2ant1 1080 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (0.‘𝐾) ∈ (Base‘𝐾))
12 eqid 2621 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
139, 12, 4atcvr0 34055 . . 3 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
14133adant3 1079 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
159, 12, 4atcvr0 34055 . . 3 ((𝐾 ∈ AtLat ∧ 𝑄𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄)
16153adant2 1078 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄)
17 atcmp.l . . 3 = (le‘𝐾)
183, 17, 12cvrcmp 34050 . 2 ((𝐾 ∈ Poset ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (0.‘𝐾) ∈ (Base‘𝐾)) ∧ ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑄)) → (𝑃 𝑄𝑃 = 𝑄))
192, 6, 8, 11, 14, 16, 18syl132anc 1341 1 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄𝑃 = 𝑄))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036   = wceq 1480  wcel 1987   class class class wbr 4613  cfv 5847  Basecbs 15781  lecple 15869  Posetcpo 16861  0.cp0 16958  ccvr 34029  Atomscatm 34030  AtLatcal 34031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-preset 16849  df-poset 16867  df-plt 16879  df-glb 16896  df-p0 16960  df-lat 16967  df-covers 34033  df-ats 34034  df-atl 34065
This theorem is referenced by:  atncmp  34079  atnlt  34080  atnle  34084  cvlsupr2  34110  cvratlem  34187  2atjm  34211  atbtwn  34212  2atm  34293  2llnmeqat  34337  dalem25  34464  dalem55  34493  dalem57  34495  snatpsubN  34516  pmapat  34529  2llnma1b  34552  cdlemblem  34559  lhp2at0nle  34801  lhpat3  34812  4atexlemcnd  34838  trlval3  34954  cdlemc5  34962  cdleme3  35004  cdleme7  35016  cdleme11k  35035  cdleme16b  35046  cdleme16e  35049  cdleme16f  35050  cdlemednpq  35066  cdleme20j  35086  cdleme22aa  35107  cdleme22cN  35110  cdleme22d  35111  cdlemf2  35330  cdlemb3  35374  cdlemg12e  35415  cdlemg17dALTN  35432  cdlemg19a  35451  cdlemg27b  35464  cdlemg31d  35468  trlcone  35496  cdlemi  35588  tendotr  35598  cdlemk17  35626  cdlemk52  35722  cdleml1N  35744  dia2dimlem1  35833  dia2dimlem2  35834  dia2dimlem3  35835
  Copyright terms: Public domain W3C validator