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 34395
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29173 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 3912 . . . 4 (𝑃𝐴 → ¬ 𝐴 = ∅)
2 atombase.a . . . . 5 𝐴 = (Atoms‘𝐾)
32eqeq1i 2625 . . . 4 (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
41, 3sylnib 318 . . 3 (𝑃𝐴 → ¬ (Atoms‘𝐾) = ∅)
5 fvprc 6172 . . 3 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
64, 5nsyl2 142 . 2 (𝑃𝐴𝐾 ∈ V)
7 atombase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2620 . . . 4 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2620 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2isat 34392 . . 3 (𝐾 ∈ V → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
1110simprbda 652 . 2 ((𝐾 ∈ V ∧ 𝑃𝐴) → 𝑃𝐵)
126, 11mpancom 702 1 (𝑃𝐴𝑃𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  Vcvv 3195  c0 3907   class class class wbr 4644  cfv 5876  Basecbs 15838  0.cp0 17018  ccvr 34368  Atomscatm 34369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fv 5884  df-ats 34373
This theorem is referenced by:  atssbase  34396  0ltat  34397  leatb  34398  meetat  34402  atnle0  34415  atlen0  34416  atcmp  34417  atcvreq0  34420  atncvrN  34421  atnle  34423  atnem0  34424  atlatmstc  34425  atlatle  34426  cvlexch2  34435  cvlexchb1  34436  cvlexchb2  34437  cvlatexchb1  34440  cvlatexchb2  34441  cvlatexch1  34442  cvlatexch2  34443  cvlatexch3  34444  cvlcvr1  34445  cvlcvrp  34446  cvlatcvr1  34447  cvlatcvr2  34448  cvlsupr2  34449  cvlsupr7  34454  cvlsupr8  34455  hlatjcl  34472  hlatjcom  34473  hlatjidm  34474  hlatjass  34475  hlatj32  34477  hlatj4  34479  hlatlej1  34480  atnlej1  34484  atnlej2  34485  hlrelat5N  34506  hlrelat  34507  hlrelat2  34508  exatleN  34509  cvr2N  34516  hlrelat3  34517  cvrval3  34518  cvrval5  34520  cvrexchlem  34524  cvratlem  34526  cvrat  34527  atcvr0eq  34531  lnnat  34532  cvrat2  34534  atcvrneN  34535  atcvrj1  34536  atcvrj2b  34537  atltcvr  34540  atle  34541  atlelt  34543  2atlt  34544  atexchcvrN  34545  cvrat3  34547  cvrat4  34548  cvrat42  34549  2atjm  34550  atbtwn  34551  3noncolr2  34554  4noncolr3  34558  athgt  34561  3dim0  34562  3dimlem3a  34565  3dimlem3OLDN  34567  3dimlem4a  34568  3dimlem4OLDN  34570  3dim3  34574  2dim  34575  1cvratex  34578  1cvrjat  34580  1cvrat  34581  ps-1  34582  ps-2  34583  hlatexch3N  34585  hlatexch4  34586  ps-2b  34587  3atlem1  34588  3atlem2  34589  3atlem4  34591  3atlem5  34592  3atlem6  34593  3at  34595  islln3  34615  llnnleat  34618  llnn0  34621  llnle  34623  llnexatN  34626  llncmp  34627  2llnmat  34629  2at0mat0  34630  2atm  34632  ps-2c  34633  lplni2  34642  lplnle  34645  lplnnle2at  34646  lplnn0N  34652  islpln2a  34653  2atmat  34666  lplnexllnN  34669  2llnjaN  34671  2llnm4  34675  2llnmeqat  34676  lvoli3  34682  islvol5  34684  lvoli2  34686  lvolnle3at  34687  3atnelvolN  34691  lvoln0N  34696  islvol2aN  34697  4atlem3  34701  4atlem3a  34702  4atlem3b  34703  4atlem4a  34704  4atlem4b  34705  4atlem4c  34706  4atlem4d  34707  4atlem9  34708  4atlem10a  34709  4atlem10  34711  4atlem11a  34712  4atlem11b  34713  4atlem11  34714  4atlem12a  34715  4atlem12b  34716  4atlem12  34717  4at2  34719  lplncvrlvol2  34720  2lplnja  34724  dalempeb  34744  dalemqeb  34745  dalemreb  34746  dalemseb  34747  dalemteb  34748  dalemueb  34749  dalem3  34769  dalem16  34784  dalemcceb  34794  dalem21  34799  dalem25  34803  dalem38  34815  dalem39  34816  dalem43  34820  dalem44  34821  dalem45  34822  dalem53  34830  dalem54  34831  dalem55  34832  dalem57  34834  dalem60  34837  snatpsubN  34855  linepsubN  34857  pmaple  34866  pmapat  34868  pmap1N  34872  pmapsub  34873  pmapglbx  34874  isline2  34879  linepmap  34880  isline3  34881  isline4N  34882  lneq2at  34883  lncvrelatN  34886  lncmp  34888  2lnat  34889  2atm2atN  34890  2llnma1b  34891  2llnma1  34892  2llnma3r  34893  cdlema1N  34896  cdlemblem  34898  cdlemb  34899  elpaddn0  34905  paddcom  34918  paddasslem2  34926  paddasslem5  34929  paddasslem12  34936  paddasslem13  34937  pmapjoin  34957  pmapjat1  34958  pmapjat2  34959  pmapjlln1  34960  atmod1i1  34962  atmod1i2  34964  llnmod1i2  34965  atmod2i1  34966  atmod2i2  34967  atmod3i1  34969  atmod3i2  34970  atmod4i1  34971  atmod4i2  34972  llnexchb2lem  34973  llnexchb2  34974  dalawlem2  34977  dalawlem3  34978  dalawlem5  34980  dalawlem6  34981  dalawlem7  34982  dalawlem8  34983  dalawlem11  34986  dalawlem12  34987  polval2N  35011  pol1N  35015  polatN  35036  2polatN  35037  paddatclN  35054  linepsubclN  35056  lhp2lt  35106  lhp0lt  35108  lhpexle2lem  35114  lhpexle3lem  35116  lhpjat2  35126  lhpj1  35127  lhpmcvr3  35130  lhpmcvr4N  35131  lhpmcvr5N  35132  lhpmcvr6N  35133  lhpmatb  35136  lhp2at0  35137  lhp2atnle  35138  lhp2at0nle  35140  lhprelat3N  35145  lhple  35147  lhpat4N  35149  lhpat3  35151  4atexlemtlw  35172  4atexlemc  35174  4atexlemnclw  35175  4atexlemcnd  35177  4atex2-0aOLDN  35183  lauteq  35200  ltrnid  35240  ltrnel  35244  ltrnat  35245  ltrncnvat  35246  ltrncnvel  35247  ltrncoval  35250  ltrncnv  35251  ltrn11at  35252  ltrneq2  35253  ltrneq  35254  idltrn  35255  ltrnmwOLD  35257  trlval2  35269  trlcnv  35271  trljat1  35272  trljat2  35273  ltrnideq  35281  arglem1N  35296  cdlemc1  35297  cdlemc2  35298  cdlemc4  35300  cdlemc5  35301  cdlemc6  35302  cdlemd1  35304  cdlemd2  35305  cdlemd3  35306  cdlemd4  35307  cdlemd7  35310  cdleme0aa  35316  cdleme0b  35318  cdleme0c  35319  cdleme0cp  35320  cdleme0cq  35321  cdleme0e  35323  cdleme0fN  35324  cdleme1b  35332  cdleme1  35333  cdleme2  35334  cdleme3b  35335  cdleme3c  35336  cdleme3e  35338  cdleme3g  35340  cdleme3h  35341  cdleme3  35343  cdleme5  35346  cdleme7d  35352  cdleme7e  35353  cdleme7ga  35354  cdleme7  35355  cdleme8  35356  cdleme9  35359  cdleme10  35360  cdleme11c  35367  cdleme11e  35369  cdleme11fN  35370  cdleme11g  35371  cdleme11k  35374  cdleme11  35376  cdleme15b  35381  cdleme15  35384  cdleme16b  35385  cdleme17b  35393  cdleme17c  35394  cdlemednpq  35405  cdleme20zN  35407  cdleme20yOLD  35409  cdleme19a  35410  cdleme20bN  35417  cdleme20d  35419  cdleme20j  35425  cdleme21c  35434  cdleme22aa  35446  cdleme22b  35448  cdleme22cN  35449  cdleme22d  35450  cdleme22e  35451  cdleme22eALTN  35452  cdleme23b  35457  cdleme23c  35458  cdleme27N  35476  cdleme28a  35477  cdleme30a  35485  cdlemefrs29pre00  35502  cdlemefrs29bpre0  35503  cdlemefrs29cpre1  35505  cdlemefrs32fva  35507  cdlemefrs32fva1  35508  cdlemefr32snb  35512  cdlemefs32snb  35522  cdleme32snb  35543  cdleme32fva  35544  cdleme32fva1  35545  cdleme32fvaw  35546  cdleme35a  35555  cdleme35fnpq  35556  cdleme35b  35557  cdleme35c  35558  cdleme35f  35561  cdleme42c  35579  cdleme42e  35586  cdleme42h  35589  cdleme42i  35590  cdleme42ke  35592  cdleme42keg  35593  cdleme42mgN  35595  cdleme17d4  35604  cdleme48fvg  35607  cdleme48bw  35609  cdlemeg46req  35636  cdleme50trn3  35660  cdlemf1  35668  cdlemf2  35669  trlord  35676  ltrniotacnvval  35689  cdlemg2fv2  35707  cdlemg2l  35710  cdlemg7fvbwN  35714  cdlemg4c  35719  cdlemg4  35724  cdlemg6c  35727  cdlemg8b  35735  cdlemg11b  35749  cdlemg13a  35758  cdlemg17a  35768  cdlemg17h  35775  cdlemg17  35784  cdlemg18b  35786  cdlemg19a  35790  cdlemg27a  35799  cdlemg27b  35803  cdlemg31a  35804  cdlemg31b  35805  cdlemg31d  35807  cdlemg33b0  35808  cdlemg33a  35813  cdlemg35  35820  trlcolem  35833  cdlemg42  35836  cdlemg44a  35838  cdlemg46  35842  cdlemh1  35922  cdlemh2  35923  cdlemh  35924  cdlemi1  35925  cdlemi  35927  cdlemk3  35940  cdlemk4  35941  cdlemkvcl  35949  cdlemk7  35955  cdlemk11  35956  cdlemk15  35962  cdlemk1u  35966  cdlemk7u  35977  cdlemk11u  35978  cdlemk37  36021  cdlemk39  36023  cdlemkid1  36029  cdlemkid2  36031  cdlemk48  36057  cdlemk50  36059  cdlemk51  36060  cdlemk52  36061  dia2dimlem1  36172  dia2dimlem2  36173  dia2dimlem3  36174  dia2dimlem5  36176  dia2dimlem7  36178  dia2dimlem9  36180  dia2dimlem10  36181  dia2dimlem12  36183  dia2dimlem13  36184  cdlemm10N  36226  cdlemn2  36303  cdlemn3  36305  cdlemn9  36313  cdlemn10  36314  dihjustlem  36324  dihord1  36326  dihord2pre2  36334  dihvalcqat  36347  dib2dim  36351  dih2dimb  36352  dih2dimbALTN  36353  dihord5apre  36370  dihglbcpreN  36408  dihmeetlem3N  36413  dihmeetlem6  36417  dihjatc1  36419  dihjatc2N  36420  dihjatc3  36421  dihmeetlem9N  36423  dihmeetlem10N  36424  dihmeetlem11N  36425  dihmeetlem13N  36427  dihmeetlem15N  36429  dihmeetlem16N  36430  dihmeetlem17N  36431  dihatexv2  36447  dihjatb  36524  dihjatc  36525  dihjatcclem1  36526  dihjatcclem2  36527  dihjatcclem4  36529  dihjat  36531  dihjat3  36540  dihjat5N  36545  dvh4dimat  36546
  Copyright terms: Public domain W3C validator