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 36533
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 30133 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 4282 . . . 4 (𝑃𝐴 → ¬ 𝐴 = ∅)
2 atombase.a . . . . 5 𝐴 = (Atoms‘𝐾)
32eqeq1i 2829 . . . 4 (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
41, 3sylnib 331 . . 3 (𝑃𝐴 → ¬ (Atoms‘𝐾) = ∅)
5 fvprc 6654 . . 3 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
64, 5nsyl2 143 . 2 (𝑃𝐴𝐾 ∈ V)
7 atombase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2824 . . . 4 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2824 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2isat 36530 . . 3 (𝐾 ∈ V → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
1110simprbda 502 . 2 ((𝐾 ∈ V ∧ 𝑃𝐴) → 𝑃𝐵)
126, 11mpancom 687 1 (𝑃𝐴𝑃𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  Vcvv 3480  c0 4276   class class class wbr 5052  cfv 6343  Basecbs 16483  0.cp0 17647  ccvr 36506  Atomscatm 36507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-iota 6302  df-fun 6345  df-fv 6351  df-ats 36511
This theorem is referenced by:  atssbase  36534  0ltat  36535  leatb  36536  meetat  36540  atnle0  36553  atlen0  36554  atcmp  36555  atcvreq0  36558  atncvrN  36559  atnle  36561  atnem0  36562  atlatmstc  36563  atlatle  36564  cvlexch2  36573  cvlexchb1  36574  cvlexchb2  36575  cvlatexchb1  36578  cvlatexchb2  36579  cvlatexch1  36580  cvlatexch2  36581  cvlatexch3  36582  cvlcvr1  36583  cvlcvrp  36584  cvlatcvr1  36585  cvlatcvr2  36586  cvlsupr2  36587  cvlsupr7  36592  cvlsupr8  36593  hlatjcl  36611  hlatjcom  36612  hlatjidm  36613  hlatjass  36614  hlatj32  36616  hlatj4  36618  hlatlej1  36619  atnlej1  36623  atnlej2  36624  hlrelat5N  36645  hlrelat  36646  hlrelat2  36647  exatleN  36648  cvr2N  36655  hlrelat3  36656  cvrval3  36657  cvrval5  36659  cvrexchlem  36663  cvratlem  36665  cvrat  36666  atcvr0eq  36670  lnnat  36671  cvrat2  36673  atcvrneN  36674  atcvrj1  36675  atcvrj2b  36676  atltcvr  36679  atle  36680  atlelt  36682  2atlt  36683  atexchcvrN  36684  cvrat3  36686  cvrat4  36687  cvrat42  36688  2atjm  36689  atbtwn  36690  3noncolr2  36693  4noncolr3  36697  athgt  36700  3dim0  36701  3dimlem3a  36704  3dimlem3OLDN  36706  3dimlem4a  36707  3dimlem4OLDN  36709  3dim3  36713  2dim  36714  1cvratex  36717  1cvrjat  36719  1cvrat  36720  ps-1  36721  ps-2  36722  hlatexch3N  36724  hlatexch4  36725  ps-2b  36726  3atlem1  36727  3atlem2  36728  3atlem4  36730  3atlem5  36731  3atlem6  36732  3at  36734  islln3  36754  llnnleat  36757  llnn0  36760  llnle  36762  llnexatN  36765  llncmp  36766  2llnmat  36768  2at0mat0  36769  2atm  36771  ps-2c  36772  lplni2  36781  lplnle  36784  lplnnle2at  36785  lplnn0N  36791  islpln2a  36792  2atmat  36805  lplnexllnN  36808  2llnjaN  36810  2llnm4  36814  2llnmeqat  36815  lvoli3  36821  islvol5  36823  lvoli2  36825  lvolnle3at  36826  3atnelvolN  36830  lvoln0N  36835  islvol2aN  36836  4atlem3  36840  4atlem3a  36841  4atlem3b  36842  4atlem4a  36843  4atlem4b  36844  4atlem4c  36845  4atlem4d  36846  4atlem9  36847  4atlem10a  36848  4atlem10  36850  4atlem11a  36851  4atlem11b  36852  4atlem11  36853  4atlem12a  36854  4atlem12b  36855  4atlem12  36856  4at2  36858  lplncvrlvol2  36859  2lplnja  36863  dalempeb  36883  dalemqeb  36884  dalemreb  36885  dalemseb  36886  dalemteb  36887  dalemueb  36888  dalem3  36908  dalem16  36923  dalemcceb  36933  dalem21  36938  dalem25  36942  dalem38  36954  dalem39  36955  dalem43  36959  dalem44  36960  dalem45  36961  dalem53  36969  dalem54  36970  dalem55  36971  dalem57  36973  dalem60  36976  snatpsubN  36994  linepsubN  36996  pmaple  37005  pmapat  37007  pmap1N  37011  pmapsub  37012  pmapglbx  37013  isline2  37018  linepmap  37019  isline3  37020  isline4N  37021  lneq2at  37022  lncvrelatN  37025  lncmp  37027  2lnat  37028  2atm2atN  37029  2llnma1b  37030  2llnma1  37031  2llnma3r  37032  cdlema1N  37035  cdlemblem  37037  cdlemb  37038  elpaddn0  37044  paddcom  37057  paddasslem2  37065  paddasslem5  37068  paddasslem12  37075  paddasslem13  37076  pmapjoin  37096  pmapjat1  37097  pmapjat2  37098  pmapjlln1  37099  atmod1i1  37101  atmod1i2  37103  llnmod1i2  37104  atmod2i1  37105  atmod2i2  37106  atmod3i1  37108  atmod3i2  37109  atmod4i1  37110  atmod4i2  37111  llnexchb2lem  37112  llnexchb2  37113  dalawlem2  37116  dalawlem3  37117  dalawlem5  37119  dalawlem6  37120  dalawlem7  37121  dalawlem8  37122  dalawlem11  37125  dalawlem12  37126  polval2N  37150  pol1N  37154  polatN  37175  2polatN  37176  paddatclN  37193  linepsubclN  37195  lhp2lt  37245  lhp0lt  37247  lhpexle2lem  37253  lhpexle3lem  37255  lhpjat2  37265  lhpj1  37266  lhpmcvr3  37269  lhpmcvr4N  37270  lhpmcvr5N  37271  lhpmcvr6N  37272  lhpmatb  37275  lhp2at0  37276  lhp2atnle  37277  lhp2at0nle  37279  lhprelat3N  37284  lhple  37286  lhpat4N  37288  lhpat3  37290  4atexlemtlw  37311  4atexlemc  37313  4atexlemnclw  37314  4atexlemcnd  37316  4atex2-0aOLDN  37322  lauteq  37339  ltrnid  37379  ltrnel  37383  ltrnat  37384  ltrncnvat  37385  ltrncnvel  37386  ltrncoval  37389  ltrncnv  37390  ltrn11at  37391  ltrneq2  37392  ltrneq  37393  idltrn  37394  trlval2  37407  trlcnv  37409  trljat1  37410  trljat2  37411  ltrnideq  37419  arglem1N  37434  cdlemc1  37435  cdlemc2  37436  cdlemc4  37438  cdlemc5  37439  cdlemc6  37440  cdlemd1  37442  cdlemd2  37443  cdlemd3  37444  cdlemd4  37445  cdlemd7  37448  cdleme0aa  37454  cdleme0b  37456  cdleme0c  37457  cdleme0cp  37458  cdleme0cq  37459  cdleme0e  37461  cdleme0fN  37462  cdleme1b  37470  cdleme1  37471  cdleme2  37472  cdleme3b  37473  cdleme3c  37474  cdleme3e  37476  cdleme3g  37478  cdleme3h  37479  cdleme3  37481  cdleme5  37484  cdleme7d  37490  cdleme7e  37491  cdleme7ga  37492  cdleme7  37493  cdleme8  37494  cdleme9  37497  cdleme10  37498  cdleme11c  37505  cdleme11e  37507  cdleme11fN  37508  cdleme11g  37509  cdleme11k  37512  cdleme11  37514  cdleme15b  37519  cdleme15  37522  cdleme16b  37523  cdleme17b  37531  cdleme17c  37532  cdlemednpq  37543  cdleme20zN  37545  cdleme19a  37547  cdleme20bN  37554  cdleme20d  37556  cdleme20j  37562  cdleme21c  37571  cdleme22aa  37583  cdleme22b  37585  cdleme22cN  37586  cdleme22d  37587  cdleme22e  37588  cdleme22eALTN  37589  cdleme23b  37594  cdleme23c  37595  cdleme27N  37613  cdleme28a  37614  cdleme30a  37622  cdlemefrs29pre00  37639  cdlemefrs29bpre0  37640  cdlemefrs29cpre1  37642  cdlemefrs32fva  37644  cdlemefrs32fva1  37645  cdlemefr32snb  37649  cdlemefs32snb  37659  cdleme32snb  37680  cdleme32fva  37681  cdleme32fva1  37682  cdleme32fvaw  37683  cdleme35a  37692  cdleme35fnpq  37693  cdleme35b  37694  cdleme35c  37695  cdleme35f  37698  cdleme42c  37716  cdleme42e  37723  cdleme42h  37726  cdleme42i  37727  cdleme42ke  37729  cdleme42keg  37730  cdleme42mgN  37732  cdleme17d4  37741  cdleme48fvg  37744  cdleme48bw  37746  cdlemeg46req  37773  cdleme50trn3  37797  cdlemf1  37805  cdlemf2  37806  trlord  37813  ltrniotacnvval  37826  cdlemg2fv2  37844  cdlemg2l  37847  cdlemg7fvbwN  37851  cdlemg4c  37856  cdlemg4  37861  cdlemg6c  37864  cdlemg8b  37872  cdlemg11b  37886  cdlemg13a  37895  cdlemg17a  37905  cdlemg17h  37912  cdlemg17  37921  cdlemg18b  37923  cdlemg19a  37927  cdlemg27a  37936  cdlemg27b  37940  cdlemg31a  37941  cdlemg31b  37942  cdlemg31d  37944  cdlemg33b0  37945  cdlemg33a  37950  cdlemg35  37957  trlcolem  37970  cdlemg42  37973  cdlemg44a  37975  cdlemg46  37979  cdlemh1  38059  cdlemh2  38060  cdlemh  38061  cdlemi1  38062  cdlemi  38064  cdlemk3  38077  cdlemk4  38078  cdlemkvcl  38086  cdlemk7  38092  cdlemk11  38093  cdlemk15  38099  cdlemk1u  38103  cdlemk7u  38114  cdlemk11u  38115  cdlemk37  38158  cdlemk39  38160  cdlemkid1  38166  cdlemkid2  38168  cdlemk48  38194  cdlemk50  38196  cdlemk51  38197  cdlemk52  38198  dia2dimlem1  38308  dia2dimlem2  38309  dia2dimlem3  38310  dia2dimlem5  38312  dia2dimlem7  38314  dia2dimlem9  38316  dia2dimlem10  38317  dia2dimlem12  38319  dia2dimlem13  38320  cdlemm10N  38362  cdlemn2  38439  cdlemn3  38441  cdlemn9  38449  cdlemn10  38450  dihjustlem  38460  dihord1  38462  dihord2pre2  38470  dihvalcqat  38483  dib2dim  38487  dih2dimb  38488  dih2dimbALTN  38489  dihord5apre  38506  dihglbcpreN  38544  dihmeetlem3N  38549  dihmeetlem6  38553  dihjatc1  38555  dihjatc2N  38556  dihjatc3  38557  dihmeetlem9N  38559  dihmeetlem10N  38560  dihmeetlem11N  38561  dihmeetlem13N  38563  dihmeetlem15N  38565  dihmeetlem16N  38566  dihmeetlem17N  38567  dihatexv2  38583  dihjatb  38660  dihjatc  38661  dihjatcclem1  38662  dihjatcclem2  38663  dihjatcclem4  38665  dihjat  38667  dihjat3  38676  dihjat5N  38681  dvh4dimat  38682
  Copyright terms: Public domain W3C validator