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

Theorem atbase 36307
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 30049 analog.) (Contributed by NM, 10-Oct-2011.)
Hypotheses
Ref Expression
atombase.b 𝐵 = (Base‘𝐾)
atombase.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
atbase (𝑃𝐴𝑃𝐵)

Proof of Theorem atbase
StepHypRef Expression
1 n0i 4298 . . . 4 (𝑃𝐴 → ¬ 𝐴 = ∅)
2 atombase.a . . . . 5 𝐴 = (Atoms‘𝐾)
32eqeq1i 2826 . . . 4 (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
41, 3sylnib 329 . . 3 (𝑃𝐴 → ¬ (Atoms‘𝐾) = ∅)
5 fvprc 6657 . . 3 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
64, 5nsyl2 143 . 2 (𝑃𝐴𝐾 ∈ V)
7 atombase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2821 . . . 4 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2821 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2isat 36304 . . 3 (𝐾 ∈ V → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
1110simprbda 499 . 2 ((𝐾 ∈ V ∧ 𝑃𝐴) → 𝑃𝐵)
126, 11mpancom 684 1 (𝑃𝐴𝑃𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  Vcvv 3495  c0 4290   class class class wbr 5058  cfv 6349  Basecbs 16473  0.cp0 17637  ccvr 36280  Atomscatm 36281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357  df-ats 36285
This theorem is referenced by:  atssbase  36308  0ltat  36309  leatb  36310  meetat  36314  atnle0  36327  atlen0  36328  atcmp  36329  atcvreq0  36332  atncvrN  36333  atnle  36335  atnem0  36336  atlatmstc  36337  atlatle  36338  cvlexch2  36347  cvlexchb1  36348  cvlexchb2  36349  cvlatexchb1  36352  cvlatexchb2  36353  cvlatexch1  36354  cvlatexch2  36355  cvlatexch3  36356  cvlcvr1  36357  cvlcvrp  36358  cvlatcvr1  36359  cvlatcvr2  36360  cvlsupr2  36361  cvlsupr7  36366  cvlsupr8  36367  hlatjcl  36385  hlatjcom  36386  hlatjidm  36387  hlatjass  36388  hlatj32  36390  hlatj4  36392  hlatlej1  36393  atnlej1  36397  atnlej2  36398  hlrelat5N  36419  hlrelat  36420  hlrelat2  36421  exatleN  36422  cvr2N  36429  hlrelat3  36430  cvrval3  36431  cvrval5  36433  cvrexchlem  36437  cvratlem  36439  cvrat  36440  atcvr0eq  36444  lnnat  36445  cvrat2  36447  atcvrneN  36448  atcvrj1  36449  atcvrj2b  36450  atltcvr  36453  atle  36454  atlelt  36456  2atlt  36457  atexchcvrN  36458  cvrat3  36460  cvrat4  36461  cvrat42  36462  2atjm  36463  atbtwn  36464  3noncolr2  36467  4noncolr3  36471  athgt  36474  3dim0  36475  3dimlem3a  36478  3dimlem3OLDN  36480  3dimlem4a  36481  3dimlem4OLDN  36483  3dim3  36487  2dim  36488  1cvratex  36491  1cvrjat  36493  1cvrat  36494  ps-1  36495  ps-2  36496  hlatexch3N  36498  hlatexch4  36499  ps-2b  36500  3atlem1  36501  3atlem2  36502  3atlem4  36504  3atlem5  36505  3atlem6  36506  3at  36508  islln3  36528  llnnleat  36531  llnn0  36534  llnle  36536  llnexatN  36539  llncmp  36540  2llnmat  36542  2at0mat0  36543  2atm  36545  ps-2c  36546  lplni2  36555  lplnle  36558  lplnnle2at  36559  lplnn0N  36565  islpln2a  36566  2atmat  36579  lplnexllnN  36582  2llnjaN  36584  2llnm4  36588  2llnmeqat  36589  lvoli3  36595  islvol5  36597  lvoli2  36599  lvolnle3at  36600  3atnelvolN  36604  lvoln0N  36609  islvol2aN  36610  4atlem3  36614  4atlem3a  36615  4atlem3b  36616  4atlem4a  36617  4atlem4b  36618  4atlem4c  36619  4atlem4d  36620  4atlem9  36621  4atlem10a  36622  4atlem10  36624  4atlem11a  36625  4atlem11b  36626  4atlem11  36627  4atlem12a  36628  4atlem12b  36629  4atlem12  36630  4at2  36632  lplncvrlvol2  36633  2lplnja  36637  dalempeb  36657  dalemqeb  36658  dalemreb  36659  dalemseb  36660  dalemteb  36661  dalemueb  36662  dalem3  36682  dalem16  36697  dalemcceb  36707  dalem21  36712  dalem25  36716  dalem38  36728  dalem39  36729  dalem43  36733  dalem44  36734  dalem45  36735  dalem53  36743  dalem54  36744  dalem55  36745  dalem57  36747  dalem60  36750  snatpsubN  36768  linepsubN  36770  pmaple  36779  pmapat  36781  pmap1N  36785  pmapsub  36786  pmapglbx  36787  isline2  36792  linepmap  36793  isline3  36794  isline4N  36795  lneq2at  36796  lncvrelatN  36799  lncmp  36801  2lnat  36802  2atm2atN  36803  2llnma1b  36804  2llnma1  36805  2llnma3r  36806  cdlema1N  36809  cdlemblem  36811  cdlemb  36812  elpaddn0  36818  paddcom  36831  paddasslem2  36839  paddasslem5  36842  paddasslem12  36849  paddasslem13  36850  pmapjoin  36870  pmapjat1  36871  pmapjat2  36872  pmapjlln1  36873  atmod1i1  36875  atmod1i2  36877  llnmod1i2  36878  atmod2i1  36879  atmod2i2  36880  atmod3i1  36882  atmod3i2  36883  atmod4i1  36884  atmod4i2  36885  llnexchb2lem  36886  llnexchb2  36887  dalawlem2  36890  dalawlem3  36891  dalawlem5  36893  dalawlem6  36894  dalawlem7  36895  dalawlem8  36896  dalawlem11  36899  dalawlem12  36900  polval2N  36924  pol1N  36928  polatN  36949  2polatN  36950  paddatclN  36967  linepsubclN  36969  lhp2lt  37019  lhp0lt  37021  lhpexle2lem  37027  lhpexle3lem  37029  lhpjat2  37039  lhpj1  37040  lhpmcvr3  37043  lhpmcvr4N  37044  lhpmcvr5N  37045  lhpmcvr6N  37046  lhpmatb  37049  lhp2at0  37050  lhp2atnle  37051  lhp2at0nle  37053  lhprelat3N  37058  lhple  37060  lhpat4N  37062  lhpat3  37064  4atexlemtlw  37085  4atexlemc  37087  4atexlemnclw  37088  4atexlemcnd  37090  4atex2-0aOLDN  37096  lauteq  37113  ltrnid  37153  ltrnel  37157  ltrnat  37158  ltrncnvat  37159  ltrncnvel  37160  ltrncoval  37163  ltrncnv  37164  ltrn11at  37165  ltrneq2  37166  ltrneq  37167  idltrn  37168  trlval2  37181  trlcnv  37183  trljat1  37184  trljat2  37185  ltrnideq  37193  arglem1N  37208  cdlemc1  37209  cdlemc2  37210  cdlemc4  37212  cdlemc5  37213  cdlemc6  37214  cdlemd1  37216  cdlemd2  37217  cdlemd3  37218  cdlemd4  37219  cdlemd7  37222  cdleme0aa  37228  cdleme0b  37230  cdleme0c  37231  cdleme0cp  37232  cdleme0cq  37233  cdleme0e  37235  cdleme0fN  37236  cdleme1b  37244  cdleme1  37245  cdleme2  37246  cdleme3b  37247  cdleme3c  37248  cdleme3e  37250  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme5  37258  cdleme7d  37264  cdleme7e  37265  cdleme7ga  37266  cdleme7  37267  cdleme8  37268  cdleme9  37271  cdleme10  37272  cdleme11c  37279  cdleme11e  37281  cdleme11fN  37282  cdleme11g  37283  cdleme11k  37286  cdleme11  37288  cdleme15b  37293  cdleme15  37296  cdleme16b  37297  cdleme17b  37305  cdleme17c  37306  cdlemednpq  37317  cdleme20zN  37319  cdleme19a  37321  cdleme20bN  37328  cdleme20d  37330  cdleme20j  37336  cdleme21c  37345  cdleme22aa  37357  cdleme22b  37359  cdleme22cN  37360  cdleme22d  37361  cdleme22e  37362  cdleme22eALTN  37363  cdleme23b  37368  cdleme23c  37369  cdleme27N  37387  cdleme28a  37388  cdleme30a  37396  cdlemefrs29pre00  37413  cdlemefrs29bpre0  37414  cdlemefrs29cpre1  37416  cdlemefrs32fva  37418  cdlemefrs32fva1  37419  cdlemefr32snb  37423  cdlemefs32snb  37433  cdleme32snb  37454  cdleme32fva  37455  cdleme32fva1  37456  cdleme32fvaw  37457  cdleme35a  37466  cdleme35fnpq  37467  cdleme35b  37468  cdleme35c  37469  cdleme35f  37472  cdleme42c  37490  cdleme42e  37497  cdleme42h  37500  cdleme42i  37501  cdleme42ke  37503  cdleme42keg  37504  cdleme42mgN  37506  cdleme17d4  37515  cdleme48fvg  37518  cdleme48bw  37520  cdlemeg46req  37547  cdleme50trn3  37571  cdlemf1  37579  cdlemf2  37580  trlord  37587  ltrniotacnvval  37600  cdlemg2fv2  37618  cdlemg2l  37621  cdlemg7fvbwN  37625  cdlemg4c  37630  cdlemg4  37635  cdlemg6c  37638  cdlemg8b  37646  cdlemg11b  37660  cdlemg13a  37669  cdlemg17a  37679  cdlemg17h  37686  cdlemg17  37695  cdlemg18b  37697  cdlemg19a  37701  cdlemg27a  37710  cdlemg27b  37714  cdlemg31a  37715  cdlemg31b  37716  cdlemg31d  37718  cdlemg33b0  37719  cdlemg33a  37724  cdlemg35  37731  trlcolem  37744  cdlemg42  37747  cdlemg44a  37749  cdlemg46  37753  cdlemh1  37833  cdlemh2  37834  cdlemh  37835  cdlemi1  37836  cdlemi  37838  cdlemk3  37851  cdlemk4  37852  cdlemkvcl  37860  cdlemk7  37866  cdlemk11  37867  cdlemk15  37873  cdlemk1u  37877  cdlemk7u  37888  cdlemk11u  37889  cdlemk37  37932  cdlemk39  37934  cdlemkid1  37940  cdlemkid2  37942  cdlemk48  37968  cdlemk50  37970  cdlemk51  37971  cdlemk52  37972  dia2dimlem1  38082  dia2dimlem2  38083  dia2dimlem3  38084  dia2dimlem5  38086  dia2dimlem7  38088  dia2dimlem9  38090  dia2dimlem10  38091  dia2dimlem12  38093  dia2dimlem13  38094  cdlemm10N  38136  cdlemn2  38213  cdlemn3  38215  cdlemn9  38223  cdlemn10  38224  dihjustlem  38234  dihord1  38236  dihord2pre2  38244  dihvalcqat  38257  dib2dim  38261  dih2dimb  38262  dih2dimbALTN  38263  dihord5apre  38280  dihglbcpreN  38318  dihmeetlem3N  38323  dihmeetlem6  38327  dihjatc1  38329  dihjatc2N  38330  dihjatc3  38331  dihmeetlem9N  38333  dihmeetlem10N  38334  dihmeetlem11N  38335  dihmeetlem13N  38337  dihmeetlem15N  38339  dihmeetlem16N  38340  dihmeetlem17N  38341  dihatexv2  38357  dihjatb  38434  dihjatc  38435  dihjatcclem1  38436  dihjatcclem2  38437  dihjatcclem4  38439  dihjat  38441  dihjat3  38450  dihjat5N  38455  dvh4dimat  38456
  Copyright terms: Public domain W3C validator