Theorem atbase 40044

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32677 analog.) (Contributed by NM, 10-Oct-2011.)

Hypotheses

Ref	Expression
atombase.b	⊢ 𝐵 = (Base‘𝐾)
atombase.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
atbase	⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Proof of Theorem atbase

Step	Hyp	Ref	Expression
1		n0i 4294	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2768	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6875	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2763	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2763	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 40041	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 503	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4287   class class class wbr 5110  ‘cfv 6538  Basecbs 17270  0.cp0 18478   ⋖ ccvr 40017  Atomscatm 40018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ats 40022

This theorem is referenced by:  atssbase  40045  0ltat  40046  leatb  40047  meetat  40051  atnle0  40064  atlen0  40065  atcmp  40066  atcvreq0  40069  atncvrN  40070  atnle  40072  atnem0  40073  atlatmstc  40074  atlatle  40075  cvlexch2  40084  cvlexchb1  40085  cvlexchb2  40086  cvlatexchb1  40089  cvlatexchb2  40090  cvlatexch1  40091  cvlatexch2  40092  cvlatexch3  40093  cvlcvr1  40094  cvlcvrp  40095  cvlatcvr1  40096  cvlatcvr2  40097  cvlsupr2  40098  cvlsupr7  40103  cvlsupr8  40104  hlatjcl  40122  hlatjcom  40123  hlatjidm  40124  hlatjass  40125  hlatj32  40127  hlatj4  40129  hlatlej1  40130  atnlej1  40134  atnlej2  40135  hlrelat5N  40156  hlrelat  40157  hlrelat2  40158  exatleN  40159  cvr2N  40166  hlrelat3  40167  cvrval3  40168  cvrval5  40170  cvrexchlem  40174  cvratlem  40176  cvrat  40177  atcvr0eq  40181  lnnat  40182  cvrat2  40184  atcvrneN  40185  atcvrj1  40186  atcvrj2b  40187  atltcvr  40190  atle  40191  atlelt  40193  2atlt  40194  atexchcvrN  40195  cvrat3  40197  cvrat4  40198  cvrat42  40199  2atjm  40200  atbtwn  40201  3noncolr2  40204  4noncolr3  40208  athgt  40211  3dim0  40212  3dimlem3a  40215  3dimlem3OLDN  40217  3dimlem4a  40218  3dimlem4OLDN  40220  3dim3  40224  2dim  40225  1cvratex  40228  1cvrjat  40230  1cvrat  40231  ps-1  40232  ps-2  40233  hlatexch3N  40235  hlatexch4  40236  ps-2b  40237  3atlem1  40238  3atlem2  40239  3atlem4  40241  3atlem5  40242  3atlem6  40243  3at  40245  islln3  40265  llnnleat  40268  llnn0  40271  llnle  40273  llnexatN  40276  llncmp  40277  2llnmat  40279  2at0mat0  40280  2atm  40282  ps-2c  40283  lplni2  40292  lplnle  40295  lplnnle2at  40296  lplnn0N  40302  islpln2a  40303  2atmat  40316  lplnexllnN  40319  2llnjaN  40321  2llnm4  40325  2llnmeqat  40326  lvoli3  40332  islvol5  40334  lvoli2  40336  lvolnle3at  40337  3atnelvolN  40341  lvoln0N  40346  islvol2aN  40347  4atlem3  40351  4atlem3a  40352  4atlem3b  40353  4atlem4a  40354  4atlem4b  40355  4atlem4c  40356  4atlem4d  40357  4atlem9  40358  4atlem10a  40359  4atlem10  40361  4atlem11a  40362  4atlem11b  40363  4atlem11  40364  4atlem12a  40365  4atlem12b  40366  4atlem12  40367  4at2  40369  lplncvrlvol2  40370  2lplnja  40374  dalempeb  40394  dalemqeb  40395  dalemreb  40396  dalemseb  40397  dalemteb  40398  dalemueb  40399  dalem3  40419  dalem16  40434  dalemcceb  40444  dalem21  40449  dalem25  40453  dalem38  40465  dalem39  40466  dalem43  40470  dalem44  40471  dalem45  40472  dalem53  40480  dalem54  40481  dalem55  40482  dalem57  40484  dalem60  40487  snatpsubN  40505  linepsubN  40507  pmaple  40516  pmapat  40518  pmap1N  40522  pmapsub  40523  pmapglbx  40524  isline2  40529  linepmap  40530  isline3  40531  isline4N  40532  lneq2at  40533  lncvrelatN  40536  lncmp  40538  2lnat  40539  2atm2atN  40540  2llnma1b  40541  2llnma1  40542  2llnma3r  40543  cdlema1N  40546  cdlemblem  40548  cdlemb  40549  elpaddn0  40555  paddcom  40568  paddasslem2  40576  paddasslem5  40579  paddasslem12  40586  paddasslem13  40587  pmapjoin  40607  pmapjat1  40608  pmapjat2  40609  pmapjlln1  40610  atmod1i1  40612  atmod1i2  40614  llnmod1i2  40615  atmod2i1  40616  atmod2i2  40617  atmod3i1  40619  atmod3i2  40620  atmod4i1  40621  atmod4i2  40622  llnexchb2lem  40623  llnexchb2  40624  dalawlem2  40627  dalawlem3  40628  dalawlem5  40630  dalawlem6  40631  dalawlem7  40632  dalawlem8  40633  dalawlem11  40636  dalawlem12  40637  polval2N  40661  pol1N  40665  polatN  40686  2polatN  40687  paddatclN  40704  linepsubclN  40706  lhp2lt  40756  lhp0lt  40758  lhpexle2lem  40764  lhpexle3lem  40766  lhpjat2  40776  lhpj1  40777  lhpmcvr3  40780  lhpmcvr4N  40781  lhpmcvr5N  40782  lhpmcvr6N  40783  lhpmatb  40786  lhp2at0  40787  lhp2atnle  40788  lhp2at0nle  40790  lhprelat3N  40795  lhple  40797  lhpat4N  40799  lhpat3  40801  4atexlemtlw  40822  4atexlemc  40824  4atexlemnclw  40825  4atexlemcnd  40827  4atex2-0aOLDN  40833  lauteq  40850  ltrnid  40890  ltrnel  40894  ltrnat  40895  ltrncnvat  40896  ltrncnvel  40897  ltrncoval  40900  ltrncnv  40901  ltrn11at  40902  ltrneq2  40903  ltrneq  40904  idltrn  40905  trlval2  40918  trlcnv  40920  trljat1  40921  trljat2  40922  ltrnideq  40930  arglem1N  40945  cdlemc1  40946  cdlemc2  40947  cdlemc4  40949  cdlemc5  40950  cdlemc6  40951  cdlemd1  40953  cdlemd2  40954  cdlemd3  40955  cdlemd4  40956  cdlemd7  40959  cdleme0aa  40965  cdleme0b  40967  cdleme0c  40968  cdleme0cp  40969  cdleme0cq  40970  cdleme0e  40972  cdleme0fN  40973  cdleme1b  40981  cdleme1  40982  cdleme2  40983  cdleme3b  40984  cdleme3c  40985  cdleme3e  40987  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme5  40995  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme8  41005  cdleme9  41008  cdleme10  41009  cdleme11c  41016  cdleme11e  41018  cdleme11fN  41019  cdleme11g  41020  cdleme11k  41023  cdleme11  41025  cdleme15b  41030  cdleme15  41033  cdleme16b  41034  cdleme17b  41042  cdleme17c  41043  cdlemednpq  41054  cdleme20zN  41056  cdleme19a  41058  cdleme20bN  41065  cdleme20d  41067  cdleme20j  41073  cdleme21c  41082  cdleme22aa  41094  cdleme22b  41096  cdleme22cN  41097  cdleme22d  41098  cdleme22e  41099  cdleme22eALTN  41100  cdleme23b  41105  cdleme23c  41106  cdleme27N  41124  cdleme28a  41125  cdleme30a  41133  cdlemefrs29pre00  41150  cdlemefrs29bpre0  41151  cdlemefrs29cpre1  41153  cdlemefrs32fva  41155  cdlemefrs32fva1  41156  cdlemefr32snb  41160  cdlemefs32snb  41170  cdleme32snb  41191  cdleme32fva  41192  cdleme32fva1  41193  cdleme32fvaw  41194  cdleme35a  41203  cdleme35fnpq  41204  cdleme35b  41205  cdleme35c  41206  cdleme35f  41209  cdleme42c  41227  cdleme42e  41234  cdleme42h  41237  cdleme42i  41238  cdleme42ke  41240  cdleme42keg  41241  cdleme42mgN  41243  cdleme17d4  41252  cdleme48fvg  41255  cdleme48bw  41257  cdlemeg46req  41284  cdleme50trn3  41308  cdlemf1  41316  cdlemf2  41317  trlord  41324  ltrniotacnvval  41337  cdlemg2fv2  41355  cdlemg2l  41358  cdlemg7fvbwN  41362  cdlemg4c  41367  cdlemg4  41372  cdlemg6c  41375  cdlemg8b  41383  cdlemg11b  41397  cdlemg13a  41406  cdlemg17a  41416  cdlemg17h  41423  cdlemg17  41432  cdlemg18b  41434  cdlemg19a  41438  cdlemg27a  41447  cdlemg27b  41451  cdlemg31a  41452  cdlemg31b  41453  cdlemg31d  41455  cdlemg33b0  41456  cdlemg33a  41461  cdlemg35  41468  trlcolem  41481  cdlemg42  41484  cdlemg44a  41486  cdlemg46  41490  cdlemh1  41570  cdlemh2  41571  cdlemh  41572  cdlemi1  41573  cdlemi  41575  cdlemk3  41588  cdlemk4  41589  cdlemkvcl  41597  cdlemk7  41603  cdlemk11  41604  cdlemk15  41610  cdlemk1u  41614  cdlemk7u  41625  cdlemk11u  41626  cdlemk37  41669  cdlemk39  41671  cdlemkid1  41677  cdlemkid2  41679  cdlemk48  41705  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  dia2dimlem1  41819  dia2dimlem2  41820  dia2dimlem3  41821  dia2dimlem5  41823  dia2dimlem7  41825  dia2dimlem9  41827  dia2dimlem10  41828  dia2dimlem12  41830  dia2dimlem13  41831  cdlemm10N  41873  cdlemn2  41950  cdlemn3  41952  cdlemn9  41960  cdlemn10  41961  dihjustlem  41971  dihord1  41973  dihord2pre2  41981  dihvalcqat  41994  dib2dim  41998  dih2dimb  41999  dih2dimbALTN  42000  dihord5apre  42017  dihglbcpreN  42055  dihmeetlem3N  42060  dihmeetlem6  42064  dihjatc1  42066  dihjatc2N  42067  dihjatc3  42068  dihmeetlem9N  42070  dihmeetlem10N  42071  dihmeetlem11N  42072  dihmeetlem13N  42074  dihmeetlem15N  42076  dihmeetlem16N  42077  dihmeetlem17N  42078  dihatexv2  42094  dihjatb  42171  dihjatc  42172  dihjatcclem1  42173  dihjatcclem2  42174  dihjatcclem4  42176  dihjat  42178  dihjat3  42187  dihjat5N  42192  dvh4dimat  42193