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 35079
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29512 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 4063 . . . 4 (𝑃𝐴 → ¬ 𝐴 = ∅)
2 atombase.a . . . . 5 𝐴 = (Atoms‘𝐾)
32eqeq1i 2765 . . . 4 (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
41, 3sylnib 317 . . 3 (𝑃𝐴 → ¬ (Atoms‘𝐾) = ∅)
5 fvprc 6346 . . 3 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
64, 5nsyl2 142 . 2 (𝑃𝐴𝐾 ∈ V)
7 atombase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2760 . . . 4 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2760 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2isat 35076 . . 3 (𝐾 ∈ V → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
1110simprbda 654 . 2 ((𝐾 ∈ V ∧ 𝑃𝐴) → 𝑃𝐵)
126, 11mpancom 706 1 (𝑃𝐴𝑃𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  Vcvv 3340  c0 4058   class class class wbr 4804  cfv 6049  Basecbs 16059  0.cp0 17238  ccvr 35052  Atomscatm 35053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-ats 35057
This theorem is referenced by:  atssbase  35080  0ltat  35081  leatb  35082  meetat  35086  atnle0  35099  atlen0  35100  atcmp  35101  atcvreq0  35104  atncvrN  35105  atnle  35107  atnem0  35108  atlatmstc  35109  atlatle  35110  cvlexch2  35119  cvlexchb1  35120  cvlexchb2  35121  cvlatexchb1  35124  cvlatexchb2  35125  cvlatexch1  35126  cvlatexch2  35127  cvlatexch3  35128  cvlcvr1  35129  cvlcvrp  35130  cvlatcvr1  35131  cvlatcvr2  35132  cvlsupr2  35133  cvlsupr7  35138  cvlsupr8  35139  hlatjcl  35156  hlatjcom  35157  hlatjidm  35158  hlatjass  35159  hlatj32  35161  hlatj4  35163  hlatlej1  35164  atnlej1  35168  atnlej2  35169  hlrelat5N  35190  hlrelat  35191  hlrelat2  35192  exatleN  35193  cvr2N  35200  hlrelat3  35201  cvrval3  35202  cvrval5  35204  cvrexchlem  35208  cvratlem  35210  cvrat  35211  atcvr0eq  35215  lnnat  35216  cvrat2  35218  atcvrneN  35219  atcvrj1  35220  atcvrj2b  35221  atltcvr  35224  atle  35225  atlelt  35227  2atlt  35228  atexchcvrN  35229  cvrat3  35231  cvrat4  35232  cvrat42  35233  2atjm  35234  atbtwn  35235  3noncolr2  35238  4noncolr3  35242  athgt  35245  3dim0  35246  3dimlem3a  35249  3dimlem3OLDN  35251  3dimlem4a  35252  3dimlem4OLDN  35254  3dim3  35258  2dim  35259  1cvratex  35262  1cvrjat  35264  1cvrat  35265  ps-1  35266  ps-2  35267  hlatexch3N  35269  hlatexch4  35270  ps-2b  35271  3atlem1  35272  3atlem2  35273  3atlem4  35275  3atlem5  35276  3atlem6  35277  3at  35279  islln3  35299  llnnleat  35302  llnn0  35305  llnle  35307  llnexatN  35310  llncmp  35311  2llnmat  35313  2at0mat0  35314  2atm  35316  ps-2c  35317  lplni2  35326  lplnle  35329  lplnnle2at  35330  lplnn0N  35336  islpln2a  35337  2atmat  35350  lplnexllnN  35353  2llnjaN  35355  2llnm4  35359  2llnmeqat  35360  lvoli3  35366  islvol5  35368  lvoli2  35370  lvolnle3at  35371  3atnelvolN  35375  lvoln0N  35380  islvol2aN  35381  4atlem3  35385  4atlem3a  35386  4atlem3b  35387  4atlem4a  35388  4atlem4b  35389  4atlem4c  35390  4atlem4d  35391  4atlem9  35392  4atlem10a  35393  4atlem10  35395  4atlem11a  35396  4atlem11b  35397  4atlem11  35398  4atlem12a  35399  4atlem12b  35400  4atlem12  35401  4at2  35403  lplncvrlvol2  35404  2lplnja  35408  dalempeb  35428  dalemqeb  35429  dalemreb  35430  dalemseb  35431  dalemteb  35432  dalemueb  35433  dalem3  35453  dalem16  35468  dalemcceb  35478  dalem21  35483  dalem25  35487  dalem38  35499  dalem39  35500  dalem43  35504  dalem44  35505  dalem45  35506  dalem53  35514  dalem54  35515  dalem55  35516  dalem57  35518  dalem60  35521  snatpsubN  35539  linepsubN  35541  pmaple  35550  pmapat  35552  pmap1N  35556  pmapsub  35557  pmapglbx  35558  isline2  35563  linepmap  35564  isline3  35565  isline4N  35566  lneq2at  35567  lncvrelatN  35570  lncmp  35572  2lnat  35573  2atm2atN  35574  2llnma1b  35575  2llnma1  35576  2llnma3r  35577  cdlema1N  35580  cdlemblem  35582  cdlemb  35583  elpaddn0  35589  paddcom  35602  paddasslem2  35610  paddasslem5  35613  paddasslem12  35620  paddasslem13  35621  pmapjoin  35641  pmapjat1  35642  pmapjat2  35643  pmapjlln1  35644  atmod1i1  35646  atmod1i2  35648  llnmod1i2  35649  atmod2i1  35650  atmod2i2  35651  atmod3i1  35653  atmod3i2  35654  atmod4i1  35655  atmod4i2  35656  llnexchb2lem  35657  llnexchb2  35658  dalawlem2  35661  dalawlem3  35662  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem11  35670  dalawlem12  35671  polval2N  35695  pol1N  35699  polatN  35720  2polatN  35721  paddatclN  35738  linepsubclN  35740  lhp2lt  35790  lhp0lt  35792  lhpexle2lem  35798  lhpexle3lem  35800  lhpjat2  35810  lhpj1  35811  lhpmcvr3  35814  lhpmcvr4N  35815  lhpmcvr5N  35816  lhpmcvr6N  35817  lhpmatb  35820  lhp2at0  35821  lhp2atnle  35822  lhp2at0nle  35824  lhprelat3N  35829  lhple  35831  lhpat4N  35833  lhpat3  35835  4atexlemtlw  35856  4atexlemc  35858  4atexlemnclw  35859  4atexlemcnd  35861  4atex2-0aOLDN  35867  lauteq  35884  ltrnid  35924  ltrnel  35928  ltrnat  35929  ltrncnvat  35930  ltrncnvel  35931  ltrncoval  35934  ltrncnv  35935  ltrn11at  35936  ltrneq2  35937  ltrneq  35938  idltrn  35939  ltrnmwOLD  35941  trlval2  35953  trlcnv  35955  trljat1  35956  trljat2  35957  ltrnideq  35965  arglem1N  35980  cdlemc1  35981  cdlemc2  35982  cdlemc4  35984  cdlemc5  35985  cdlemc6  35986  cdlemd1  35988  cdlemd2  35989  cdlemd3  35990  cdlemd4  35991  cdlemd7  35994  cdleme0aa  36000  cdleme0b  36002  cdleme0c  36003  cdleme0cp  36004  cdleme0cq  36005  cdleme0e  36007  cdleme0fN  36008  cdleme1b  36016  cdleme1  36017  cdleme2  36018  cdleme3b  36019  cdleme3c  36020  cdleme3e  36022  cdleme3g  36024  cdleme3h  36025  cdleme3  36027  cdleme5  36030  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme8  36040  cdleme9  36043  cdleme10  36044  cdleme11c  36051  cdleme11e  36053  cdleme11fN  36054  cdleme11g  36055  cdleme11k  36058  cdleme11  36060  cdleme15b  36065  cdleme15  36068  cdleme16b  36069  cdleme17b  36077  cdleme17c  36078  cdlemednpq  36089  cdleme20zN  36091  cdleme19a  36093  cdleme20bN  36100  cdleme20d  36102  cdleme20j  36108  cdleme21c  36117  cdleme22aa  36129  cdleme22b  36131  cdleme22cN  36132  cdleme22d  36133  cdleme22e  36134  cdleme22eALTN  36135  cdleme23b  36140  cdleme23c  36141  cdleme27N  36159  cdleme28a  36160  cdleme30a  36168  cdlemefrs29pre00  36185  cdlemefrs29bpre0  36186  cdlemefrs29cpre1  36188  cdlemefrs32fva  36190  cdlemefrs32fva1  36191  cdlemefr32snb  36195  cdlemefs32snb  36205  cdleme32snb  36226  cdleme32fva  36227  cdleme32fva1  36228  cdleme32fvaw  36229  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35c  36241  cdleme35f  36244  cdleme42c  36262  cdleme42e  36269  cdleme42h  36272  cdleme42i  36273  cdleme42ke  36275  cdleme42keg  36276  cdleme42mgN  36278  cdleme17d4  36287  cdleme48fvg  36290  cdleme48bw  36292  cdlemeg46req  36319  cdleme50trn3  36343  cdlemf1  36351  cdlemf2  36352  trlord  36359  ltrniotacnvval  36372  cdlemg2fv2  36390  cdlemg2l  36393  cdlemg7fvbwN  36397  cdlemg4c  36402  cdlemg4  36407  cdlemg6c  36410  cdlemg8b  36418  cdlemg11b  36432  cdlemg13a  36441  cdlemg17a  36451  cdlemg17h  36458  cdlemg17  36467  cdlemg18b  36469  cdlemg19a  36473  cdlemg27a  36482  cdlemg27b  36486  cdlemg31a  36487  cdlemg31b  36488  cdlemg31d  36490  cdlemg33b0  36491  cdlemg33a  36496  cdlemg35  36503  trlcolem  36516  cdlemg42  36519  cdlemg44a  36521  cdlemg46  36525  cdlemh1  36605  cdlemh2  36606  cdlemh  36607  cdlemi1  36608  cdlemi  36610  cdlemk3  36623  cdlemk4  36624  cdlemkvcl  36632  cdlemk7  36638  cdlemk11  36639  cdlemk15  36645  cdlemk1u  36649  cdlemk7u  36660  cdlemk11u  36661  cdlemk37  36704  cdlemk39  36706  cdlemkid1  36712  cdlemkid2  36714  cdlemk48  36740  cdlemk50  36742  cdlemk51  36743  cdlemk52  36744  dia2dimlem1  36855  dia2dimlem2  36856  dia2dimlem3  36857  dia2dimlem5  36859  dia2dimlem7  36861  dia2dimlem9  36863  dia2dimlem10  36864  dia2dimlem12  36866  dia2dimlem13  36867  cdlemm10N  36909  cdlemn2  36986  cdlemn3  36988  cdlemn9  36996  cdlemn10  36997  dihjustlem  37007  dihord1  37009  dihord2pre2  37017  dihvalcqat  37030  dib2dim  37034  dih2dimb  37035  dih2dimbALTN  37036  dihord5apre  37053  dihglbcpreN  37091  dihmeetlem3N  37096  dihmeetlem6  37100  dihjatc1  37102  dihjatc2N  37103  dihjatc3  37104  dihmeetlem9N  37106  dihmeetlem10N  37107  dihmeetlem11N  37108  dihmeetlem13N  37110  dihmeetlem15N  37112  dihmeetlem16N  37113  dihmeetlem17N  37114  dihatexv2  37130  dihjatb  37207  dihjatc  37208  dihjatcclem1  37209  dihjatcclem2  37210  dihjatcclem4  37212  dihjat  37214  dihjat3  37223  dihjat5N  37228  dvh4dimat  37229
  Copyright terms: Public domain W3C validator