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 35098
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29543 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 4068 . . . 4 (𝑃𝐴 → ¬ 𝐴 = ∅)
2 atombase.a . . . . 5 𝐴 = (Atoms‘𝐾)
32eqeq1i 2776 . . . 4 (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
41, 3sylnib 317 . . 3 (𝑃𝐴 → ¬ (Atoms‘𝐾) = ∅)
5 fvprc 6326 . . 3 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
64, 5nsyl2 144 . 2 (𝑃𝐴𝐾 ∈ V)
7 atombase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2771 . . . 4 (0.‘𝐾) = (0.‘𝐾)
9 eqid 2771 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2isat 35095 . . 3 (𝐾 ∈ V → (𝑃𝐴 ↔ (𝑃𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
1110simprbda 486 . 2 ((𝐾 ∈ V ∧ 𝑃𝐴) → 𝑃𝐵)
126, 11mpancom 668 1 (𝑃𝐴𝑃𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  Vcvv 3351  c0 4063   class class class wbr 4786  cfv 6031  Basecbs 16064  0.cp0 17245  ccvr 35071  Atomscatm 35072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-ats 35076
This theorem is referenced by:  atssbase  35099  0ltat  35100  leatb  35101  meetat  35105  atnle0  35118  atlen0  35119  atcmp  35120  atcvreq0  35123  atncvrN  35124  atnle  35126  atnem0  35127  atlatmstc  35128  atlatle  35129  cvlexch2  35138  cvlexchb1  35139  cvlexchb2  35140  cvlatexchb1  35143  cvlatexchb2  35144  cvlatexch1  35145  cvlatexch2  35146  cvlatexch3  35147  cvlcvr1  35148  cvlcvrp  35149  cvlatcvr1  35150  cvlatcvr2  35151  cvlsupr2  35152  cvlsupr7  35157  cvlsupr8  35158  hlatjcl  35175  hlatjcom  35176  hlatjidm  35177  hlatjass  35178  hlatj32  35180  hlatj4  35182  hlatlej1  35183  atnlej1  35187  atnlej2  35188  hlrelat5N  35209  hlrelat  35210  hlrelat2  35211  exatleN  35212  cvr2N  35219  hlrelat3  35220  cvrval3  35221  cvrval5  35223  cvrexchlem  35227  cvratlem  35229  cvrat  35230  atcvr0eq  35234  lnnat  35235  cvrat2  35237  atcvrneN  35238  atcvrj1  35239  atcvrj2b  35240  atltcvr  35243  atle  35244  atlelt  35246  2atlt  35247  atexchcvrN  35248  cvrat3  35250  cvrat4  35251  cvrat42  35252  2atjm  35253  atbtwn  35254  3noncolr2  35257  4noncolr3  35261  athgt  35264  3dim0  35265  3dimlem3a  35268  3dimlem3OLDN  35270  3dimlem4a  35271  3dimlem4OLDN  35273  3dim3  35277  2dim  35278  1cvratex  35281  1cvrjat  35283  1cvrat  35284  ps-1  35285  ps-2  35286  hlatexch3N  35288  hlatexch4  35289  ps-2b  35290  3atlem1  35291  3atlem2  35292  3atlem4  35294  3atlem5  35295  3atlem6  35296  3at  35298  islln3  35318  llnnleat  35321  llnn0  35324  llnle  35326  llnexatN  35329  llncmp  35330  2llnmat  35332  2at0mat0  35333  2atm  35335  ps-2c  35336  lplni2  35345  lplnle  35348  lplnnle2at  35349  lplnn0N  35355  islpln2a  35356  2atmat  35369  lplnexllnN  35372  2llnjaN  35374  2llnm4  35378  2llnmeqat  35379  lvoli3  35385  islvol5  35387  lvoli2  35389  lvolnle3at  35390  3atnelvolN  35394  lvoln0N  35399  islvol2aN  35400  4atlem3  35404  4atlem3a  35405  4atlem3b  35406  4atlem4a  35407  4atlem4b  35408  4atlem4c  35409  4atlem4d  35410  4atlem9  35411  4atlem10a  35412  4atlem10  35414  4atlem11a  35415  4atlem11b  35416  4atlem11  35417  4atlem12a  35418  4atlem12b  35419  4atlem12  35420  4at2  35422  lplncvrlvol2  35423  2lplnja  35427  dalempeb  35447  dalemqeb  35448  dalemreb  35449  dalemseb  35450  dalemteb  35451  dalemueb  35452  dalem3  35472  dalem16  35487  dalemcceb  35497  dalem21  35502  dalem25  35506  dalem38  35518  dalem39  35519  dalem43  35523  dalem44  35524  dalem45  35525  dalem53  35533  dalem54  35534  dalem55  35535  dalem57  35537  dalem60  35540  snatpsubN  35558  linepsubN  35560  pmaple  35569  pmapat  35571  pmap1N  35575  pmapsub  35576  pmapglbx  35577  isline2  35582  linepmap  35583  isline3  35584  isline4N  35585  lneq2at  35586  lncvrelatN  35589  lncmp  35591  2lnat  35592  2atm2atN  35593  2llnma1b  35594  2llnma1  35595  2llnma3r  35596  cdlema1N  35599  cdlemblem  35601  cdlemb  35602  elpaddn0  35608  paddcom  35621  paddasslem2  35629  paddasslem5  35632  paddasslem12  35639  paddasslem13  35640  pmapjoin  35660  pmapjat1  35661  pmapjat2  35662  pmapjlln1  35663  atmod1i1  35665  atmod1i2  35667  llnmod1i2  35668  atmod2i1  35669  atmod2i2  35670  atmod3i1  35672  atmod3i2  35673  atmod4i1  35674  atmod4i2  35675  llnexchb2lem  35676  llnexchb2  35677  dalawlem2  35680  dalawlem3  35681  dalawlem5  35683  dalawlem6  35684  dalawlem7  35685  dalawlem8  35686  dalawlem11  35689  dalawlem12  35690  polval2N  35714  pol1N  35718  polatN  35739  2polatN  35740  paddatclN  35757  linepsubclN  35759  lhp2lt  35809  lhp0lt  35811  lhpexle2lem  35817  lhpexle3lem  35819  lhpjat2  35829  lhpj1  35830  lhpmcvr3  35833  lhpmcvr4N  35834  lhpmcvr5N  35835  lhpmcvr6N  35836  lhpmatb  35839  lhp2at0  35840  lhp2atnle  35841  lhp2at0nle  35843  lhprelat3N  35848  lhple  35850  lhpat4N  35852  lhpat3  35854  4atexlemtlw  35875  4atexlemc  35877  4atexlemnclw  35878  4atexlemcnd  35880  4atex2-0aOLDN  35886  lauteq  35903  ltrnid  35943  ltrnel  35947  ltrnat  35948  ltrncnvat  35949  ltrncnvel  35950  ltrncoval  35953  ltrncnv  35954  ltrn11at  35955  ltrneq2  35956  ltrneq  35957  idltrn  35958  ltrnmwOLD  35960  trlval2  35972  trlcnv  35974  trljat1  35975  trljat2  35976  ltrnideq  35984  arglem1N  35999  cdlemc1  36000  cdlemc2  36001  cdlemc4  36003  cdlemc5  36004  cdlemc6  36005  cdlemd1  36007  cdlemd2  36008  cdlemd3  36009  cdlemd4  36010  cdlemd7  36013  cdleme0aa  36019  cdleme0b  36021  cdleme0c  36022  cdleme0cp  36023  cdleme0cq  36024  cdleme0e  36026  cdleme0fN  36027  cdleme1b  36035  cdleme1  36036  cdleme2  36037  cdleme3b  36038  cdleme3c  36039  cdleme3e  36041  cdleme3g  36043  cdleme3h  36044  cdleme3  36046  cdleme5  36049  cdleme7d  36055  cdleme7e  36056  cdleme7ga  36057  cdleme7  36058  cdleme8  36059  cdleme9  36062  cdleme10  36063  cdleme11c  36070  cdleme11e  36072  cdleme11fN  36073  cdleme11g  36074  cdleme11k  36077  cdleme11  36079  cdleme15b  36084  cdleme15  36087  cdleme16b  36088  cdleme17b  36096  cdleme17c  36097  cdlemednpq  36108  cdleme20zN  36110  cdleme19a  36112  cdleme20bN  36119  cdleme20d  36121  cdleme20j  36127  cdleme21c  36136  cdleme22aa  36148  cdleme22b  36150  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22eALTN  36154  cdleme23b  36159  cdleme23c  36160  cdleme27N  36178  cdleme28a  36179  cdleme30a  36187  cdlemefrs29pre00  36204  cdlemefrs29bpre0  36205  cdlemefrs29cpre1  36207  cdlemefrs32fva  36209  cdlemefrs32fva1  36210  cdlemefr32snb  36214  cdlemefs32snb  36224  cdleme32snb  36245  cdleme32fva  36246  cdleme32fva1  36247  cdleme32fvaw  36248  cdleme35a  36257  cdleme35fnpq  36258  cdleme35b  36259  cdleme35c  36260  cdleme35f  36263  cdleme42c  36281  cdleme42e  36288  cdleme42h  36291  cdleme42i  36292  cdleme42ke  36294  cdleme42keg  36295  cdleme42mgN  36297  cdleme17d4  36306  cdleme48fvg  36309  cdleme48bw  36311  cdlemeg46req  36338  cdleme50trn3  36362  cdlemf1  36370  cdlemf2  36371  trlord  36378  ltrniotacnvval  36391  cdlemg2fv2  36409  cdlemg2l  36412  cdlemg7fvbwN  36416  cdlemg4c  36421  cdlemg4  36426  cdlemg6c  36429  cdlemg8b  36437  cdlemg11b  36451  cdlemg13a  36460  cdlemg17a  36470  cdlemg17h  36477  cdlemg17  36486  cdlemg18b  36488  cdlemg19a  36492  cdlemg27a  36501  cdlemg27b  36505  cdlemg31a  36506  cdlemg31b  36507  cdlemg31d  36509  cdlemg33b0  36510  cdlemg33a  36515  cdlemg35  36522  trlcolem  36535  cdlemg42  36538  cdlemg44a  36540  cdlemg46  36544  cdlemh1  36624  cdlemh2  36625  cdlemh  36626  cdlemi1  36627  cdlemi  36629  cdlemk3  36642  cdlemk4  36643  cdlemkvcl  36651  cdlemk7  36657  cdlemk11  36658  cdlemk15  36664  cdlemk1u  36668  cdlemk7u  36679  cdlemk11u  36680  cdlemk37  36723  cdlemk39  36725  cdlemkid1  36731  cdlemkid2  36733  cdlemk48  36759  cdlemk50  36761  cdlemk51  36762  cdlemk52  36763  dia2dimlem1  36874  dia2dimlem2  36875  dia2dimlem3  36876  dia2dimlem5  36878  dia2dimlem7  36880  dia2dimlem9  36882  dia2dimlem10  36883  dia2dimlem12  36885  dia2dimlem13  36886  cdlemm10N  36928  cdlemn2  37005  cdlemn3  37007  cdlemn9  37015  cdlemn10  37016  dihjustlem  37026  dihord1  37028  dihord2pre2  37036  dihvalcqat  37049  dib2dim  37053  dih2dimb  37054  dih2dimbALTN  37055  dihord5apre  37072  dihglbcpreN  37110  dihmeetlem3N  37115  dihmeetlem6  37119  dihjatc1  37121  dihjatc2N  37122  dihjatc3  37123  dihmeetlem9N  37125  dihmeetlem10N  37126  dihmeetlem11N  37127  dihmeetlem13N  37129  dihmeetlem15N  37131  dihmeetlem16N  37132  dihmeetlem17N  37133  dihatexv2  37149  dihjatb  37226  dihjatc  37227  dihjatcclem1  37228  dihjatcclem2  37229  dihjatcclem4  37231  dihjat  37233  dihjat3  37242  dihjat5N  37247  dvh4dimat  37248
  Copyright terms: Public domain W3C validator