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 37062
Description: If two atoms are comparable, they are equal. (atsseq 30428 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 37052 . . 3 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
213ad2ant1 1135 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → 𝐾 ∈ Poset)
3 eqid 2737 . . . 4 (Base‘𝐾) = (Base‘𝐾)
4 atcmp.a . . . 4 𝐴 = (Atoms‘𝐾)
53, 4atbase 37040 . . 3 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
653ad2ant2 1136 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → 𝑃 ∈ (Base‘𝐾))
73, 4atbase 37040 . . 3 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
873ad2ant3 1137 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → 𝑄 ∈ (Base‘𝐾))
9 eqid 2737 . . . 4 (0.‘𝐾) = (0.‘𝐾)
103, 9atl0cl 37054 . . 3 (𝐾 ∈ AtLat → (0.‘𝐾) ∈ (Base‘𝐾))
11103ad2ant1 1135 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (0.‘𝐾) ∈ (Base‘𝐾))
12 eqid 2737 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
139, 12, 4atcvr0 37039 . . 3 ((𝐾 ∈ AtLat ∧ 𝑃𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
14133adant3 1134 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
159, 12, 4atcvr0 37039 . . 3 ((𝐾 ∈ AtLat ∧ 𝑄𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄)
16153adant2 1133 . 2 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄)
17 atcmp.l . . 3 = (le‘𝐾)
183, 17, 12cvrcmp 37034 . 2 ((𝐾 ∈ Poset ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (0.‘𝐾) ∈ (Base‘𝐾)) ∧ ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑄)) → (𝑃 𝑄𝑃 = 𝑄))
192, 6, 8, 11, 14, 16, 18syl132anc 1390 1 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄𝑃 = 𝑄))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  w3a 1089   = wceq 1543  wcel 2110   class class class wbr 5053  cfv 6380  Basecbs 16760  lecple 16809  Posetcpo 17814  0.cp0 17929  ccvr 37013  Atomscatm 37014  AtLatcal 37015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-proset 17802  df-poset 17820  df-plt 17836  df-glb 17853  df-p0 17931  df-lat 17938  df-covers 37017  df-ats 37018  df-atl 37049
This theorem is referenced by:  atncmp  37063  atnlt  37064  atnle  37068  cvlsupr2  37094  cvratlem  37172  2atjm  37196  atbtwn  37197  2atm  37278  2llnmeqat  37322  dalem25  37449  dalem55  37478  dalem57  37480  snatpsubN  37501  pmapat  37514  2llnma1b  37537  cdlemblem  37544  lhp2at0nle  37786  lhpat3  37797  4atexlemcnd  37823  trlval3  37938  cdlemc5  37946  cdleme3  37988  cdleme7  38000  cdleme11k  38019  cdleme16b  38030  cdleme16e  38033  cdleme16f  38034  cdlemednpq  38050  cdleme20j  38069  cdleme22aa  38090  cdleme22cN  38093  cdleme22d  38094  cdlemf2  38313  cdlemb3  38357  cdlemg12e  38398  cdlemg17dALTN  38415  cdlemg19a  38434  cdlemg27b  38447  cdlemg31d  38451  trlcone  38479  cdlemi  38571  tendotr  38581  cdlemk17  38609  cdlemk52  38705  cdleml1N  38727  dia2dimlem1  38815  dia2dimlem2  38816  dia2dimlem3  38817
  Copyright terms: Public domain W3C validator