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 34056
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29052 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 3896 . . . 4 (𝑃𝐴 → ¬ 𝐴 = ∅)
2 atombase.a . . . . 5 𝐴 = (Atoms‘𝐾)
32eqeq1i 2626 . . . 4 (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
41, 3sylnib 318 . . 3 (𝑃𝐴 → ¬ (Atoms‘𝐾) = ∅)
5 fvprc 6142 . . 3 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
64, 5nsyl2 142 . 2 (𝑃𝐴𝐾 ∈ V)
7 atombase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2621 . . . 4 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2621 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2isat 34053 . . 3 (𝐾 ∈ V → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
1110simprbda 652 . 2 ((𝐾 ∈ V ∧ 𝑃𝐴) → 𝑃𝐵)
126, 11mpancom 702 1 (𝑃𝐴𝑃𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  Vcvv 3186  c0 3891   class class class wbr 4613  cfv 5847  Basecbs 15781  0.cp0 16958  ccvr 34029  Atomscatm 34030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-ats 34034
This theorem is referenced by:  atssbase  34057  0ltat  34058  leatb  34059  meetat  34063  atnle0  34076  atlen0  34077  atcmp  34078  atcvreq0  34081  atncvrN  34082  atnle  34084  atnem0  34085  atlatmstc  34086  atlatle  34087  cvlexch2  34096  cvlexchb1  34097  cvlexchb2  34098  cvlatexchb1  34101  cvlatexchb2  34102  cvlatexch1  34103  cvlatexch2  34104  cvlatexch3  34105  cvlcvr1  34106  cvlcvrp  34107  cvlatcvr1  34108  cvlatcvr2  34109  cvlsupr2  34110  cvlsupr7  34115  cvlsupr8  34116  hlatjcl  34133  hlatjcom  34134  hlatjidm  34135  hlatjass  34136  hlatj32  34138  hlatj4  34140  hlatlej1  34141  atnlej1  34145  atnlej2  34146  hlrelat5N  34167  hlrelat  34168  hlrelat2  34169  exatleN  34170  cvr2N  34177  hlrelat3  34178  cvrval3  34179  cvrval5  34181  cvrexchlem  34185  cvratlem  34187  cvrat  34188  atcvr0eq  34192  lnnat  34193  cvrat2  34195  atcvrneN  34196  atcvrj1  34197  atcvrj2b  34198  atltcvr  34201  atle  34202  atlelt  34204  2atlt  34205  atexchcvrN  34206  cvrat3  34208  cvrat4  34209  cvrat42  34210  2atjm  34211  atbtwn  34212  3noncolr2  34215  4noncolr3  34219  athgt  34222  3dim0  34223  3dimlem3a  34226  3dimlem3OLDN  34228  3dimlem4a  34229  3dimlem4OLDN  34231  3dim3  34235  2dim  34236  1cvratex  34239  1cvrjat  34241  1cvrat  34242  ps-1  34243  ps-2  34244  hlatexch3N  34246  hlatexch4  34247  ps-2b  34248  3atlem1  34249  3atlem2  34250  3atlem4  34252  3atlem5  34253  3atlem6  34254  3at  34256  islln3  34276  llnnleat  34279  llnn0  34282  llnle  34284  llnexatN  34287  llncmp  34288  2llnmat  34290  2at0mat0  34291  2atm  34293  ps-2c  34294  lplni2  34303  lplnle  34306  lplnnle2at  34307  lplnn0N  34313  islpln2a  34314  2atmat  34327  lplnexllnN  34330  2llnjaN  34332  2llnm4  34336  2llnmeqat  34337  lvoli3  34343  islvol5  34345  lvoli2  34347  lvolnle3at  34348  3atnelvolN  34352  lvoln0N  34357  islvol2aN  34358  4atlem3  34362  4atlem3a  34363  4atlem3b  34364  4atlem4a  34365  4atlem4b  34366  4atlem4c  34367  4atlem4d  34368  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem11b  34374  4atlem11  34375  4atlem12a  34376  4atlem12b  34377  4atlem12  34378  4at2  34380  lplncvrlvol2  34381  2lplnja  34385  dalempeb  34405  dalemqeb  34406  dalemreb  34407  dalemseb  34408  dalemteb  34409  dalemueb  34410  dalem3  34430  dalem16  34445  dalemcceb  34455  dalem21  34460  dalem25  34464  dalem38  34476  dalem39  34477  dalem43  34481  dalem44  34482  dalem45  34483  dalem53  34491  dalem54  34492  dalem55  34493  dalem57  34495  dalem60  34498  snatpsubN  34516  linepsubN  34518  pmaple  34527  pmapat  34529  pmap1N  34533  pmapsub  34534  pmapglbx  34535  isline2  34540  linepmap  34541  isline3  34542  isline4N  34543  lneq2at  34544  lncvrelatN  34547  lncmp  34549  2lnat  34550  2atm2atN  34551  2llnma1b  34552  2llnma1  34553  2llnma3r  34554  cdlema1N  34557  cdlemblem  34559  cdlemb  34560  elpaddn0  34566  paddcom  34579  paddasslem2  34587  paddasslem5  34590  paddasslem12  34597  paddasslem13  34598  pmapjoin  34618  pmapjat1  34619  pmapjat2  34620  pmapjlln1  34621  atmod1i1  34623  atmod1i2  34625  llnmod1i2  34626  atmod2i1  34627  atmod2i2  34628  atmod3i1  34630  atmod3i2  34631  atmod4i1  34632  atmod4i2  34633  llnexchb2lem  34634  llnexchb2  34635  dalawlem2  34638  dalawlem3  34639  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem11  34647  dalawlem12  34648  polval2N  34672  pol1N  34676  polatN  34697  2polatN  34698  paddatclN  34715  linepsubclN  34717  lhp2lt  34767  lhp0lt  34769  lhpexle2lem  34775  lhpexle3lem  34777  lhpjat2  34787  lhpj1  34788  lhpmcvr3  34791  lhpmcvr4N  34792  lhpmcvr5N  34793  lhpmcvr6N  34794  lhpmatb  34797  lhp2at0  34798  lhp2atnle  34799  lhp2at0nle  34801  lhprelat3N  34806  lhple  34808  lhpat4N  34810  lhpat3  34812  4atexlemtlw  34833  4atexlemc  34835  4atexlemnclw  34836  4atexlemcnd  34838  4atex2-0aOLDN  34844  lauteq  34861  ltrnid  34901  ltrnel  34905  ltrnat  34906  ltrncnvat  34907  ltrncnvel  34908  ltrncoval  34911  ltrncnv  34912  ltrn11at  34913  ltrneq2  34914  ltrneq  34915  idltrn  34916  ltrnmwOLD  34918  trlval2  34930  trlcnv  34932  trljat1  34933  trljat2  34934  ltrnideq  34942  arglem1N  34957  cdlemc1  34958  cdlemc2  34959  cdlemc4  34961  cdlemc5  34962  cdlemc6  34963  cdlemd1  34965  cdlemd2  34966  cdlemd3  34967  cdlemd4  34968  cdlemd7  34971  cdleme0aa  34977  cdleme0b  34979  cdleme0c  34980  cdleme0cp  34981  cdleme0cq  34982  cdleme0e  34984  cdleme0fN  34985  cdleme1b  34993  cdleme1  34994  cdleme2  34995  cdleme3b  34996  cdleme3c  34997  cdleme3e  34999  cdleme3g  35001  cdleme3h  35002  cdleme3  35004  cdleme5  35007  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme7  35016  cdleme8  35017  cdleme9  35020  cdleme10  35021  cdleme11c  35028  cdleme11e  35030  cdleme11fN  35031  cdleme11g  35032  cdleme11k  35035  cdleme11  35037  cdleme15b  35042  cdleme15  35045  cdleme16b  35046  cdleme17b  35054  cdleme17c  35055  cdlemednpq  35066  cdleme20zN  35068  cdleme20yOLD  35070  cdleme19a  35071  cdleme20bN  35078  cdleme20d  35080  cdleme20j  35086  cdleme21c  35095  cdleme22aa  35107  cdleme22b  35109  cdleme22cN  35110  cdleme22d  35111  cdleme22e  35112  cdleme22eALTN  35113  cdleme23b  35118  cdleme23c  35119  cdleme27N  35137  cdleme28a  35138  cdleme30a  35146  cdlemefrs29pre00  35163  cdlemefrs29bpre0  35164  cdlemefrs29cpre1  35166  cdlemefrs32fva  35168  cdlemefrs32fva1  35169  cdlemefr32snb  35173  cdlemefs32snb  35183  cdleme32snb  35204  cdleme32fva  35205  cdleme32fva1  35206  cdleme32fvaw  35207  cdleme35a  35216  cdleme35fnpq  35217  cdleme35b  35218  cdleme35c  35219  cdleme35f  35222  cdleme42c  35240  cdleme42e  35247  cdleme42h  35250  cdleme42i  35251  cdleme42ke  35253  cdleme42keg  35254  cdleme42mgN  35256  cdleme17d4  35265  cdleme48fvg  35268  cdleme48bw  35270  cdlemeg46req  35297  cdleme50trn3  35321  cdlemf1  35329  cdlemf2  35330  trlord  35337  ltrniotacnvval  35350  cdlemg2fv2  35368  cdlemg2l  35371  cdlemg7fvbwN  35375  cdlemg4c  35380  cdlemg4  35385  cdlemg6c  35388  cdlemg8b  35396  cdlemg11b  35410  cdlemg13a  35419  cdlemg17a  35429  cdlemg17h  35436  cdlemg17  35445  cdlemg18b  35447  cdlemg19a  35451  cdlemg27a  35460  cdlemg27b  35464  cdlemg31a  35465  cdlemg31b  35466  cdlemg31d  35468  cdlemg33b0  35469  cdlemg33a  35474  cdlemg35  35481  trlcolem  35494  cdlemg42  35497  cdlemg44a  35499  cdlemg46  35503  cdlemh1  35583  cdlemh2  35584  cdlemh  35585  cdlemi1  35586  cdlemi  35588  cdlemk3  35601  cdlemk4  35602  cdlemkvcl  35610  cdlemk7  35616  cdlemk11  35617  cdlemk15  35623  cdlemk1u  35627  cdlemk7u  35638  cdlemk11u  35639  cdlemk37  35682  cdlemk39  35684  cdlemkid1  35690  cdlemkid2  35692  cdlemk48  35718  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  dia2dimlem1  35833  dia2dimlem2  35834  dia2dimlem3  35835  dia2dimlem5  35837  dia2dimlem7  35839  dia2dimlem9  35841  dia2dimlem10  35842  dia2dimlem12  35844  dia2dimlem13  35845  cdlemm10N  35887  cdlemn2  35964  cdlemn3  35966  cdlemn9  35974  cdlemn10  35975  dihjustlem  35985  dihord1  35987  dihord2pre2  35995  dihvalcqat  36008  dib2dim  36012  dih2dimb  36013  dih2dimbALTN  36014  dihord5apre  36031  dihglbcpreN  36069  dihmeetlem3N  36074  dihmeetlem6  36078  dihjatc1  36080  dihjatc2N  36081  dihjatc3  36082  dihmeetlem9N  36084  dihmeetlem10N  36085  dihmeetlem11N  36086  dihmeetlem13N  36088  dihmeetlem15N  36090  dihmeetlem16N  36091  dihmeetlem17N  36092  dihatexv2  36108  dihjatb  36185  dihjatc  36186  dihjatcclem1  36187  dihjatcclem2  36188  dihjatcclem4  36190  dihjat  36192  dihjat3  36201  dihjat5N  36206  dvh4dimat  36207
  Copyright terms: Public domain W3C validator